From f4bd0d01fc2b3382b38c25a5582c6debc78db4ef Mon Sep 17 00:00:00 2001 From: Nathan Whitehead Date: Mon, 9 Mar 2026 11:29:42 -0700 Subject: [PATCH] Make config general --- lake-manifest.json | 2 +- lakefile.toml | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index e11fc9f..c5b6153 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,5 +1,5 @@ {"version": "1.1.0", - "packagesDir": "/Users/heartpunk/.lake-shared/packages", + "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", diff --git a/lakefile.toml b/lakefile.toml index 68f4af7..4c3ee9b 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,7 +1,6 @@ name = "learnability" version = "0.1.0" keywords = ["math"] -packagesDir = "/Users/heartpunk/.lake-shared/packages" defaultTargets = ["LTS", "ConditionalSimulation", "Convergence", "Learnability", "CoinductiveBisimulation", "LearnabilityConvergence"] [leanOptions]