feat: move Lean4Packages content to submodules (#47)

Author: kim-em

.gitmodules

@@ -0,0 +1,6 @@
+[submodule "Lean4Packages/mathlib3port"]
+	path = Lean4Packages/mathlib3port
+	url = [email protected]:leanprover-community/mathlib3port.git
+[submodule "Lean4Packages/lean3port"]
+	path = Lean4Packages/lean3port
+	url = [email protected]:leanprover-community/lean3port.git

Lean4Packages/lean3port

@@ -90,11 +90,11 @@ build:
 
 port-lean: init-logs build
 	LEAN_PATH=$(MATHPORT_LIB):$(MATHLIB4_LIB):$(LEANBIN_LIB) ./build/bin/mathport config.json Leanbin::all >> Logs/mathport.out 2> >(tee -a Logs/mathport.err >&2)
-	cp lean-toolchain Lean4Packages/leanbin/
+	cp lean-toolchain Lean4Packages/lean3port/
 
 port-mathbin: port-lean
 	LEAN_PATH=$(MATHPORT_LIB):$(MATHLIB4_LIB):$(LEANBIN_LIB):$(MATHBIN_LIB) ./build/bin/mathport config.json Leanbin::all Mathbin::all >> Logs/mathport.out 2> >(tee -a Logs/mathport.err >&2)
-	cp lean-toolchain Lean4Packages/mathbin/
+	cp lean-toolchain Lean4Packages/mathlib3port/
 
 test-import-leanbin:
 	cd Test/importLeanbin && rm -rf build lean_packages && lake build

Lean4Packages/leanbin/Leanbin.lean

@@ -5,5 +5,20 @@ 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
 
-See the `Makefile` for usage (it takes several hours to rebuild the mathlib port),
-or the `test-mathport` repository if you'd prefer to use a pre-built artifact.
+## Running mathport locally
+
+See the `Makefile` for usage (it takes several hours to rebuild the mathlib port).
+
+## Running with artifacts from continuous integration
+
+To avoid having to run `mathport` locally, we provide downloadable files
+containing the `.lean` files and `.olean` files generated from Lean 3 and from mathlib3.
+
+The directory `Lean4Packages` contains subdirectories `lean3port` and `mathlib3port`,
+which are in fact git submodules,
+each containing a `lakefile.lean` that automatically obtains
+the relevant generated `.olean` files from a tarball.
+
+The directory `Test` contains subdirectories `importLeanBin` and `importMathbin`,
+each containing a `lakefile.lean` that depends on one of the projects
+from the `Lean4Packages` directory.

Lean4Packages/leanbin/lakefile.lean

@@ -5,7 +5,6 @@ open Lake DSL System
 package importLeanbin where
   defaultFacet := PackageFacet.oleans
   dependencies := #[{
-    name := "leanbin",
-    src := Source.git "https://github.com/leanprover-community/mathport.git" "master",
-    dir := "Lean4Packages/leanbin"
+    name := "lean3port",
+    src := Source.git "https://github.com/leanprover-community/lean3port.git" "master"
   }]

Lean4Packages/leanbin/lean-toolchain

@@ -5,7 +5,6 @@ open Lake DSL System
 package importMathbin where
   defaultFacet := PackageFacet.oleans
   dependencies := #[{
-    name := "mathbin",
-    src := Source.git "https://github.com/leanprover-community/mathport.git" "master",
-    dir := "Lean4Packages/mathbin"
+    name := "mathlib3port",
+    src := Source.git "https://github.com/leanprover-community/mathlib3port.git" "master"
   }]