search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
40 stars 15 forks source link

Update Makefile to increment depth of Lean history #253

Closed agjftucker closed 10 months ago

agjftucker commented 10 months ago

Mathlib 3 is currently using a version of Lean 3 one commit behind Master.

digama0 commented 10 months ago

I would rather this be fixed by either bumping mathlib3, or downloading the exact right version of lean for mathlib3 in this makefile. Downloading 2 versions is not a sustainable fix.

agjftucker commented 10 months ago

Downloading 2 versions is not a sustainable fix.

I completely agree! However I am not sufficiently qualified in make/bash/git to design a better solution. The purpose of this PR was only really to draw attention to the issue, which causes a fatal error when following the standard instructions.

I would rather this be fixed by either bumping mathlib3, or downloading the exact right version of lean for mathlib3 in this makefile.

I briefly entertained the idea that I might implement your second option simply by copying the git init/remote add/fetch origin $$REV trick from further down in the makefile, but I couldn't work out how to get the full commit hash of the Lean used by mathlib.