feat: self-contained Makefile (#30)

Author: kim-em

.docker/Dockerfile

@@ -0,0 +1,70 @@
+# This Dockerfile mostly exists to verify that the Makefile works;
+# it's unlikely that we'll actually use it "in production"!
+# You may also need to allow the Docker engine a lot of memory (32gb?)
+FROM ubuntu
+
+USER root
+
+# Set timezone to UTC to avoid prompts from tzdata.
+RUN TZ=UTC ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
+# Install prerequisites.
+RUN apt-get update && \
+    apt-get install -y git libgmp-dev cmake ccache gcc-10 g++-10 && \
+    apt-get install -y build-essential && \
+    apt-get install -y curl python3-yaml python3 python-is-python3 && \
+    apt-get clean
+
+# create a non-root user
+RUN useradd -m lean
+
+USER lean
+WORKDIR /home/lean
+
+SHELL ["/bin/bash", "-c"]
+# set the entrypoint to be a login shell, so everything is on the PATH
+ENTRYPOINT ["/bin/bash", "-l"]
+
+# make sure binaries are available even in non-login shells
+ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"
+
+## TODO: Once `lake` is distributed as part of Lean4, hopefully we can just install `elan`:
+# install elan
+# RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y && \
+#     . ~/.profile && \
+#     elan toolchain uninstall stable
+
+## For now, we need to grab an old version of `elan-init` and build `lake` ourselves:
+
+RUN curl -L https://github.com/leanprover/elan/releases/download/v1.0.8/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tar.gz && \
+    tar zxf elan.tar.gz && \
+    rm elan.tar.gz && \
+    ./elan-init -y && \
+    . ~/.profile && \
+    elan toolchain uninstall stable
+
+# We need to set CC and CCX while building lake.
+ENV CC="gcc-10"
+ENV CXX="g++-10"
+
+RUN mkdir -p /home/lean/.local/bin
+RUN git clone https://github.com/leanprover/lake && \
+    cd lake && \
+    ./build.sh && \
+    ln -s /home/lean/lake/build/bin/lake /home/lean/.local/bin/lake
+
+# TODO: switch back to the main mathport repository once the Makefile PR merges.
+RUN git clone https://github.com/semorrison/mathport --branch Makefile
+WORKDIR /home/lean/mathport
+
+# We need to set CC and CCX while building lean3 / lean4.
+ENV CC="gcc-10"
+ENV CXX="g++-10"
+
+RUN make mathbin-source
+RUN make lean3-source
+RUN make lean4-source
+RUN make lean3-predata
+RUN make mathbin-predata
+RUN make build
+RUN make port-lean
+RUN make port-mathbin

.gitignore

@@ -4,3 +4,5 @@ build/
 Logs/
 PreData/
 Lib4/*/
+lean_packages/
+sources/

Makefile

@@ -1,9 +1,95 @@
+### Makefile for mathport
+
+# This is not a "real" makefile, i.e. it does not detect dependencies between targets.
+
+## Targets:
+# `lean4-source`: clone `lean4`, patch `kernel/inductive.cpp`, compile, and `elan override`
+# `mathbin-source`: clone mathlib3, and create `all.lean`
+# `lean3-source`: clone lean3, and create `all.lean` (run after `mathbin-source`, to get the right commit)
+# `lean3-predata`: create `.ast` and `.tlean` files from Lean3
+# `mathbin-predata`: create `.ast` and `.tlean` files from mathlib3
+# `build`: compile mathport
+# `port-lean`: run mathport on Lean3
+# `port-mathbin`: run mathport on mathlib3
+
+## Prerequisites:
+# curl, git, cmake, elan, python3
+
+# We make the following assumptions about versions:
+#
+# * `lean-toolchain` points to the same version of `lean4` as
+#    the branch/commit of `mathlib4` selected in `lakefile.lean`.
+#
+# It will automatically identify the version of `lean3` than `mathlib` currently uses.
+
 all:
 
 unport:
 	rm -rf Lib4 Logs/*
 	git checkout HEAD -- Lib4
 
+# Select which commit of mathlib3 to use.
+MATHBIN_COMMIT=master
+
+# Unfortunately we can't use vanilla lean4: we need to cherrypick
+# https://github.com/dselsam/lean4/commit/9228d3949bda8c1411e707b3e20650fa1fdb9b4d
+lean4-source:
+	rm -rf sources/lean4
+	mkdir -p sources
+	cd sources && git clone --depth 1 --branch `cat ../lean-toolchain | sed "s/.*://"` https://github.com/leanprover/lean4-nightly/ lean4
+	cd sources/lean4 && git submodule update --init src/lake
+	cd sources/lean4 && patch -u src/kernel/inductive.cpp < ../../whnf-type-inductives.patch
+	cd sources/lean4 && rm -rf build && mkdir -p build/release && cd build/release && \
+	  cmake ../.. && make -j`python -c 'import multiprocessing as mp; print(mp.cpu_count())'`
+	elan toolchain link lean4-mathport-cherrypick sources/lean4/build/release/stage1/
+	elan override set lean4-mathport-cherrypick
+
+# Obtain the requested commit from `mathlib`, and create `all.lean`
+mathbin-source:
+	mkdir -p sources
+	if [ ! -d "sources/mathlib" ]; then \
+		cd sources && git clone https://github.com/leanprover-community/mathlib.git; \
+	fi
+	cd sources/mathlib && git clean -xfd && git checkout $(MATHBIN_COMMIT)
+	cd sources/mathlib && leanpkg configure && ./scripts/mk_all.sh
+
+# Obtain the commit from (community edition) Lean 3 which mathlib is using, and create `all.lean`.
+lean3-source:
+	mkdir -p sources
+	if [ ! -d "sources/lean" ]; then \
+		cd sources && git clone 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
+	# Run cmake, to create `version.lean` from `version.lean.in`.
+	cd sources/lean/build/release && cmake ../../src
+	# Create `all.lean`.
+	./mk_all.sh sources/lean/library/
+
+# Build .ast and .tlean files for Lean 3
+lean3-predata: lean3-source
+	mkdir -p PreData
+	rm -rf PreData/Leanbin
+	find sources/lean/library -name "*.olean" -delete # ast only exported when oleans not present
+	# FIXME replace `stable` here with what mathlib is using?
+	cd sources/lean && elan override set stable
+	cd sources/lean && lean --make --recursive --ast --tlean library
+	cp -r sources/lean/library PreData/Leanbin
+	find PreData/ -name "*.lean" -delete
+	find PreData/ -name "*.olean" -delete
+
+# Build .ast and .tlean files for Mathlib 3.
+mathbin-predata: mathbin-source
+	rm -rf PreData/Mathbin
+	find sources/mathlib -name "*.olean" -delete # ast only exported when oleans not present
+	# By changing into the directory, `elan` automatically dispatches to the correct binary.
+	cd sources/mathlib && lean --make --recursive --ast --tlean src
+	cp -r sources/mathlib PreData/Mathbin
+	find PreData/ -name "*.lean" -delete
+	find PreData/ -name "*.olean" -delete
+
+predata: lean3-predata mathbin-predata
+
 init-logs:
 	mkdir -p Logs
 
@@ -12,57 +98,22 @@ MATHPORT_LIB=./build/lib
 
 LEANBIN_LIB=./Lib4/leanbin/build/lib
 MATHBIN_LIB=./Lib4/mathbin/build/lib
-LIQUIDBIN_LIB=./Lib4/liquidbin/build/lib
 
-port-lean: init-logs
-	LEAN_PATH=$(MATHPORT_LIB):$(MATHLIB4_LIB):$(LEANBIN_LIB) time ./build/bin/mathport config.json Leanbin::all >> Logs/mathport.out 2> Logs/mathport.err
+build:
+	lake 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> Logs/mathport.err
 	LEAN_PATH=$(MATHPORT_LIB):$(MATHLIB4_LIB):$(LEANBIN_LIB) lean --o=$(LEANBIN_LIB)/Leanbin.olean ./Lib4/leanbin/Leanbin.lean
 	cp lean-toolchain Lib4/leanbin
 
-port-mathlib: port-lean
-	LEAN_PATH=$(MATHPORT_LIB):$(MATHLIB4_LIB):$(LEANBIN_LIB):$(MATHBIN_LIB) time ./build/bin/mathport config.json Leanbin::all Mathbin::all >> Logs/mathport.out 2> Logs/mathport.err
+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> Logs/mathport.err
 	LEAN_PATH=$(MATHPORT_LIB):$(MATHLIB4_LIB):$(LEANBIN_LIB):$(MATHBIN_LIB) lean  --o=$(MATHBIN_LIB)/Mathbin.olean ./Lib4/mathbin/Mathbin.lean
 	cp lean-toolchain Lib4/mathbin
 
-port-liquid: port-mathlib
-	LEAN_PATH=$(MATHPORT_LIB):$(MATHLIB4_LIB):$(LEANBIN_LIB):$(MATHBIN_LIB):$(LIQUIDBIN_LIB) time ./build/bin/mathport config.json Leanbin::all Mathbin::all Liquidbin::all >> Logs/mathport.out 2> Logs/mathport.err
-	LEAN_PATH=$(MATHPORT_LIB):$(MATHLIB4_LIB):$(LEANBIN_LIB):$(MATHBIN_LIB):$(LIQUIDBIN_LIB) lean  --o=$(LIQUIDBIN_LIB)/Liquidbin.olean ./Lib4/liquidbin/Liquidbin.lean
-	cp lean-toolchain Lib4/liquidbin
+test:
+	LEAN_PATH=$(MATHPORT_LIB):$(MATHLIB4_LIB):$(LEANBIN_LIB):$(MATHBIN_LIB) lean ./Test.lean
 
 tar-lib4:
 	tar --exclude 'lean_packages' -czvf mathport-release.tar.gz Lib4 Logs PreData
-
-lean3-predata:
-	mkdir -p PreData
-	rm -rf PreData/Leanbin
-	find $(LEAN3_LIB) -name "*.olean" -delete # ast only exported when oleans not present
-	LEAN_PATH=$(LEAN3_LIB)                 $(LEAN3_BIN)/lean --make --recursive --ast --tlean $(LEAN3_LIB)
-	LEAN_PATH=$(LEAN3_LIB):$(LEAN3_PKG)    $(LEAN3_BIN)/lean --make --recursive --ast --tlean $(LEAN3_PKG)
-	cp -r $(LEAN3_LIB) PreData/Leanbin
-	find PreData/ -name "*.lean" -delete
-	find PreData/ -name "*.olean" -delete
-
-mathbin-predata: lean3-predata
-	rm -rf PreData/Mathbin
-	find $(MATHLIB3_SRC) -name "*.olean" -delete # ast only exported when oleans not present
-	LEAN_PATH=$(LEAN3_LIB):$(MATHLIB3_SRC)  $(LEAN3_BIN)/lean --make --recursive --ast   $(MATHLIB3_SRC)
-	LEAN_PATH=$(LEAN3_LIB):$(MATHLIB3_SRC)  $(LEAN3_BIN)/lean --make --recursive --tlean $(MATHLIB3_SRC)
-	cp -r $(MATHLIB3_SRC) PreData/Mathbin
-	find PreData/ -name "*.lean" -delete
-	find PreData/ -name "*.olean" -delete
-
-liquid-predata: mathbin-predata
-	rm -rf PreData/Liquid
-	find $(LIQUID3_SRC) -name "*.olean" -delete # ast only exported when oleans not present
-	LEAN_PATH=$(LEAN3_LIB):$(MATHLIB3_SRC):$(LIQUID3_SRC) $(LEAN3_BIN)/lean --make --recursive --ast --tlean $(LIQUID3_SRC)
-	cp -r $(LIQUID3_SRC) PreData/Liquidbin
-	find PreData/ -name "*.lean" -delete
-	find PreData/ -name "*.olean" -delete
-
-tmp-liquid-predata:
-	rm -rf PreData/Liquid
-	find $(LIQUID3_SRC) -name "*.olean" -delete # ast only exported when oleans not present
-	LEAN_PATH=$(LEAN3_LIB):$(MATHLIB3_SRC):$(LIQUID3_SRC) $(LEAN3_BIN)/lean --make --recursive --ast --tlean $(LIQUID3_SRC)
-	cp -r $(LIQUID3_SRC) PreData/Liquidbin
-	find PreData/ -name "*.lean" -delete
-	find PreData/ -name "*.olean" -delete

Mathport/Prelude/Syntax.lean

@@ -217,7 +217,6 @@ syntax (name := async) "async " tacticSeq : tactic
 
 namespace Conv
 
-syntax (name := first) "first " withPosition((group(colGe "|" convSeq))+) : conv
 macro "try " t:convSeq : conv => `(first | $t | skip)
 syntax "runConv " doSeq : conv
 

README.md

@@ -4,3 +4,6 @@ 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.

Test.lean

@@ -0,0 +1,10 @@
+import Mathlib
+import Mathbin
+
+#check Semiring
+#lookup3 semiring
+#check Semiringₓ
+
+#lookup3 nat.exists_infinite_primes
+
+example (n : Nat) : n + n = 2 * n := by ring

config.json

@@ -3,8 +3,7 @@
         "outRoot": "Lib4",
         "packages": {
             "Leanbin": "PreData/Leanbin",
-            "Mathbin": "PreData/Mathbin",
-            "Liquidbin": "PreData/Liquidbin"
+            "Mathbin": "PreData/Mathbin/src"
         }
     },
     "stringsToKeep": [

lakefile.lean

@@ -5,9 +5,17 @@ open Lake DSL System
 package mathport {
   dependencies := #[{
     name := "mathlib",
-    src := Source.git "https://github.com/dselsam/mathlib4.git" "lake" none,
+    -- We point to a particular commit in mathlib4,
+    -- as changes to tactics in mathlib4 often cause breakages here,
+    -- particularly in `Mathport/Syntax/Translate/Tactic/Mathlib.lean`.
+    -- We'll need to keep updating that file, and bumping the commit here.
+    src := Source.git "https://github.com/leanprover-community/mathlib4.git" "b28a3d51e722d8b43367035e0eb5790b4cb6da53",
     dir := FilePath.mk "."
   }],
   binRoot := `MathportApp
-  linkArgs := #["-rdynamic"]
+  moreLinkArgs :=
+    if Platform.isWindows then
+      #["-Wl,--export-all"]
+    else
+      #["-rdynamic"]
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2021-10-02
+leanprover/lean4:nightly-2021-10-16

mathlib

@@ -0,0 +1 @@
+Subproject commit c33b823e24ba6307f7a2cdaf1cead76a7029a14d

mk_all.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+# Usage: mk_all.sh [subdirectory]
+#
+
+cd $1
+find . -name \*.lean -not -name all.lean \
+  | sed 's,^\./,,;s,\.lean$,,;s,/,.,g;s,^,import ,' \
+  | sort > ./all.lean

whnf-type-inductives.patch

@@ -0,0 +1,54 @@
+From 9228d3949bda8c1411e707b3e20650fa1fdb9b4d Mon Sep 17 00:00:00 2001
+From: Daniel Selsam <[email protected]>
+Date: Sat, 23 Jan 2021 15:00:09 -0800
+Subject: [PATCH] temp: whnf the type of inductives
+
+---
+ src/kernel/inductive.cpp | 8 +++++++-
+ 1 file changed, 7 insertions(+), 1 deletion(-)
+
+diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp
+index 3d1a47659b..9c48383c36 100644
+--- a/src/kernel/inductive.cpp
++++ b/src/kernel/inductive.cpp
+@@ -168,6 +168,7 @@ public:
+             tc().check(type, m_lparams);
+             m_nindices.push_back(0);
+             unsigned i = 0;
++            type = whnf(type);
+             while (is_pi(type)) {
+                 if (i < m_nparams) {
+                     if (first) {
+@@ -181,9 +182,11 @@ public:
+                     }
+                     i++;
+                 } else {
+-                    type = binding_body(type);
++                    expr index = mk_local_decl_for(type);
++                    type = instantiate(binding_body(type), index);
+                     m_nindices.back()++;
+                 }
++                type = whnf(type);
+             }
+             if (i != m_nparams)
+                 throw kernel_exception(m_env, "number of parameters mismatch in inductive datatype declaration");
+@@ -527,6 +530,8 @@ public:
+             rec_info info;
+             expr t      = ind_type.get_type();
+             unsigned i  = 0;
++
++            t = whnf(t);
+             while (is_pi(t)) {
+                 if (i < m_nparams) {
+                     t = instantiate(binding_body(t), m_params[i]);
+@@ -536,6 +541,7 @@ public:
+                     t = instantiate(binding_body(t), idx);
+                 }
+                 i++;
++                t = whnf(t);
+             }
+             info.m_major = mk_local_decl("t", mk_app(mk_app(m_ind_cnsts[d_idx], m_params), info.m_indices));
+             expr C_ty = mk_sort(m_elim_level);
+--
+2.30.1 (Apple Git-130)
+