update instructions for external projects (#237)

leanprover-community · May 29, 2023 · 49ea836 · 49ea836
1 parent afeb177
commit 49ea836
Show file tree

Hide file tree

Showing 5 changed files with 197 additions and 17 deletions.
diff --git a/Makefile b/Makefile
@@ -43,7 +43,7 @@ MATHBIN_COMMIT=origin/master
 mathbin-source:
 	mkdir -p sources
 	if [ ! -d "sources/mathlib/.git" ]; then \
-		cd sources && git clone https://github.com/leanprover-community/mathlib.git; \
+		cd sources && git clone --depth 1 https://github.com/leanprover-community/mathlib.git; \
 	fi
 	cd sources/mathlib && git clean -xfd && git fetch && git checkout "$(MATHBIN_COMMIT)" --
 	cd sources/mathlib && echo -n 'mathlib commit: ' && git rev-parse HEAD
@@ -56,7 +56,7 @@ mathbin-source:
 lean3-source: mathbin-source
 	mkdir -p sources
 	if [ ! -d "sources/lean/.git" ]; then \
-		cd sources && git clone https://github.com/leanprover-community/lean.git; \
+		cd sources && git clone --depth 1 https://github.com/leanprover-community/lean.git; \
 	fi
 	cd sources/lean && git clean -xfd && git checkout "`cd ../mathlib && lean --version | sed -e "s/.*commit \([0-9a-f]*\).*/\1/"`" --
 	mkdir -p sources/lean/build/release

diff --git a/Oneshot/README.md b/Oneshot/README.md
@@ -8,11 +8,19 @@ This is a template which you can use to quickly play with the translation of sni
    ```
 2. get in the folder: `cd mathport`
 3. install dependencies `cmake`, `gmp`, `gmp-devel`, `jq` if needed (debian/ubuntu `sudo apt install cmake gmp gmp-devel jq`, mac `brew install cmake jq`, etc)
-4. Run `make build`
-5. Run `make lean3-source`
-6. Get a mathport release with `./download-release.sh $my_choice`, where $mychoice = `nightly-2022-12-13-04` works, **or just** `./download-release.sh` to get the latest one automatically.
-7. Put Lean 3 code in `Oneshot/lean3-in/main.lean`.
-8. Put extra `#align` in `Oneshot/lean4-in/Oneshot.lean`
-9. Run `make oneshot`
+4. Run `lake exe cache get`
+5. Run `make build` (go get some coffee!)
+6. Run `make lean3-source`
+7. Get a mathport release with `./download-release.sh $my_choice`, where $my_choice = `nightly-2022-12-13-04` works, **or just** `./download-release.sh` to get the latest one automatically.
+8. Put Lean 3 code in `Oneshot/lean3-in/main.lean`.
+9. Put extra `#align` in `Oneshot/lean4-in/Oneshot.lean`
+10. Run `make oneshot`
 
-After the first run, you only have to repeat steps 7-9, unless you want to update mathlib (step 6) or mathport itself (`git pull` and then steps 4-9).
+After the first run, you only have to repeat steps 8-10, unless you want to update mathlib (step 7) or mathport itself (`git pull` and then steps 4-10).
+
+If things work, at the end you should see
+`# output is in Outputs/src/oneshot/Oneshot/Main.lean`.
+You may need to add `import Mathlib.Mathport.Rename` to this file
+before the `#align` commands work.
+Also, all you mathlib imports will say `import Mathbin.XYZ`,
+and need to be changed to `import Mathlib.XYZ`.
diff --git a/README.md b/README.md
@@ -5,6 +5,103 @@ Mathport is a tool for porting Lean3 projects to Lean4. It consists of two (loos
 - "binport", which translates Lean3 `.lean` files to Lean4 `.olean` files
 - "synport", which best-effort translates Lean3 `.lean` files to Lean4 `.lean` files
 
+## Running on mathlib
+
+If you want to port a file from mathlib to mathlib4, you don't need anything here.
+Instead you should go to the mathlib4 repository, and use `scripts/start_port.sh`.
+
+## Running on a single file
+
+Mathport supports a "oneshot" mode, for porting individual files or quick tests.
+A template is set up in the `Oneshot/` directory. See [`Oneshot/README.md`](Oneshot/README.md).
+
+## Running on a project other than mathlib
+
+Install dependencies if needed:
+
+- debian/ubuntu: `sudo apt install cmake gmp gmp-devel jq`
+- mac: `brew install cmake jq`
+
+In the mathport folder:
+
+- `lake exe cache get`
+- `make build`
+  This step is somewhat expensive as we need to compile (not just build)
+  all of the dependencies of tactics.
+- `make source`
+- `./download-release.sh`
+  (Or `./download-release.sh [relevant-release]`
+  if you need to run against an old mathlib;
+  see [mathport releases](https://github.com/leanprover-community/mathport/releases),
+  and find the nearest `nightly`.)
+
+Make sure that your project is using the same version of Lean 3 as the latest
+mathlib3, if at all possible.
+Similarly bump your mathlib dependency to the lastest mathlib3 if possible.
+
+If you really want to run against an older mathlib3 (good luck!):
+
+- In `sources/mathlib` run `git --fetch unshallow`
+- `git checkout SHA` for the mathlib3 SHA you need.
+- `leanproject get-cache`
+
+Next, you'll need to prepare your project.
+It is probably best to clone a fresh copy for this
+(outside of the `mathport` directory).
+
+In your project, run:
+
+- `leanproject mk-all`
+- make sure that `leanproject build` runs cleanly.
+- In `leanpkg.path`, change the line `path _target/deps/mathlib/src` to
+  `path ../mathport/sources/mathlib/src`
+  (this should be the relative path from your project
+  to mathport's copy of `mathlib/src`.)
+- `leanproject clean`
+- `lean --make --recursive --ast --tlean src` (get coffee).
+
+Now, in mathport, edit `config-project.json` as follows:
+
+- Under `pathConfig/packages/`, change the string after the `"Project"` key
+  to the relative path from the mathport directory to your
+  external project's `src/` directory.
+
+Then run
+
+- `./build/bin/mathport --make config-project.json Project::all`
+
+If it succeeds, you should find Lean4 lean files in `Outputs/src/project/`.
+(Note this may be hidden in the VS Code explorer,
+but you can open it in the terminal.)
+
+If you need to re-run mathport, you will need to `rm -rf Outputs/olean/project`.
+
+If the generated Lean files look plausible,
+you will want to move them into a new Lean 4 project.
+
+Somewhere outside of the `mathport` folder, run
+`lake +leanprover/lean4:nightly-2023-05-22 init MyProject math`
+(probably updating `nightly-2023-05-22`
+to match the toolchain in current `mathlib4`).
+Then you can `mv Outputs/src/project/Project ../MyProject/MyProject`,
+and then inside `MyProject` run `lake update` and `lake exe cache get`.
+
+You will need to edit the imports to change
+`import Mathbin.XYZ` to `import Mathlib.XYZ`.
+
+Depending on the layout of your project, you may need to adjust imports
+or create secondary libraries in your `lakefile.lean`, e.g.
+```
+lean_lib ForMathlib where
+  roots := #[`ForMathlib]
+```
+
+After that you should be able to edit files in VS Code,
+and begin fixing remaining errors.
+
+Please expect errors if any of your filenames require escaping via `«...»`.
+(In particular if your filenames start with numerals.)
+
 ## Running with artifacts from continuous integration
 
 A full run of `mathport` (see below) on Lean 3 and mathlib3 takes several hours.
@@ -16,19 +113,22 @@ Please use the repositories
 https://github.com/leanprover-community/lean3port
 and
 https://github.com/leanprover-community/mathlib3port
-and run `lake build` to obtain the generated `.olean` files.
+and run `lake exe cache get` and then
+`lake build` to obtain the generated `.olean` files.
 
 Using these repositories, you can open the synported `.lean` files in VS Code
 to see the current state of output.
 
 Alternatively, you can import some or all of the binported `.olean` files
 using e.g.
-```
+
+```lean
 import Mathbin.AlgebraicGeometry.Scheme
 
 #lookup3 algebraic_geometry.Scheme
 #check AlgebraicGeometry.Scheme
 ```
+
 (Specifying the `mathlib3port` repository as a Lake dependency in your own
 project should work to enable `import Mathbin.All`.)
 
@@ -48,7 +148,10 @@ where `<tag>` is a release from https://github.com/leanprover-community/mathport
 ## Running mathport locally
 
 See the `Makefile` for usage (it takes several hours to rebuild the mathlib3 port from scratch).
-Basic usage is `make build source predata port`.
+Basic usage is `lake exe cache get` and then `make build source`.
+
+After that you can try just `make predata port`,
+but you probably should download artifacts first as described below.
 
 We provide artifacts for various stages of the build on the releases page of the `mathport` repository.
 The script `./download-release.sh nightly-YYYY-MM-DD` downloads one of these,
@@ -68,5 +171,3 @@ To port a single file execute `mathport` as follows
 
 The directory `Test` contains subdirectories `importLeanBin` and `importMathbin`,
 each containing a `lakefile.lean` that depends on `lean3port` and `mathlib3port`, resp.
-
-Mathport also supports a "oneshot" mode, for quick tests. A template is set up in the `Oneshot/` directory. See [`Oneshot/README.md`](Oneshot/README.md).
diff --git a/config-project.json b/config-project.json
@@ -0,0 +1,71 @@
+{
+    "pathConfig": {
+        "outRoot": "Outputs",
+        "packages": {
+            "Leanbin": "sources/lean/library",
+            "Mathbin": "sources/mathlib/src",
+            "Oneshot": "Oneshot/lean3-in",
+            "Project": "../lean-liquid/src"
+        },
+        "leanPath": [
+            "./lake-packages/mathlib/build/lib",
+            "./lake-packages/Qq/build/lib",
+            "./lake-packages/std/build/lib",
+            "./lake-packages/aesop/build/lib",
+            "./Oneshot/lean4-in/build/lib",
+            "./Outputs/oleans/leanbin",
+            "./Outputs/oleans/mathbin",
+            "./Outputs/oleans/oneshot",
+            "./Outputs/oleans/project"
+        ]
+    },
+    "baseModules": ["Mathlib"],
+    "extraModules": [],
+    "stringsToKeep": [
+        "_sunfold",
+        "equations",
+        "private",
+        "below",
+        "ibelow"
+    ],
+    "forceAbbrevs": [
+        "lift",
+        "lift_t",
+        "coe_b",
+        "coe_t",
+        "coe_fn_b"
+    ],
+    "defEqConstructions": [],
+    "defEqConstructions-disabled-because-sometimes-different-in-lean4": [
+        "casesOn",
+        "noConfusion",
+        "ibelow",
+        "brecOn",
+        "bInductionOn"
+    ],
+    "disabledInstances": [
+        "bool.decidable_eq",
+        "nat.decidable_eq",
+        "and.decidable",
+        "or.decidable",
+        "iff.decidable",
+        "not.decidable",
+        "implies.decidable",
+        "decidable.true",
+        "decidable.false",
+        "exists_prop_decidable",
+        "forall_prop_decidable",
+        "int.decidable_eq",
+        "nat.decidable_lt",
+        "nat.decidable_le"
+    ],
+    "neverSorries": [
+        "of_as_true"
+    ],
+    "sorries": [],
+    "skipProofs": false,
+    "skipDefEq": true,
+    "replacementStyle": "comment",
+    "redundantAlign": false,
+    "error2warning" : true
+}
diff --git a/download-predata.sh b/download-predata.sh
@@ -1,11 +1,11 @@
 #!/usr/bin/env bash
 # Script to download artifacts from a release.
-# Usage: `./download-predata.sh nightly-predata-2021-11-30`
+# Usage: `./download-predata.sh nightly-2021-11-30`
 
-RELEASE=$1    # e.g. nightly-predata-2021-11-30
+RELEASE=$1    # e.g. nightly-2021-11-30
 
 if [ -z "$RELEASE" ]; then
-    echo "Usage: ./download-predata.sh nightly-predata-YYYY-MM-DD"
+    echo "Usage: ./download-predata.sh predata-nightly-YYYY-MM-DD"
     echo "See https://github.com/leanprover-community/mathport/releases for available releases"
     exit 1
 fi