issues setting up leanblueprint

Stream: general

[Alex Brodbelt]

Hi!

I was thinking of writing up my formalization in either verso or using the lean blueprint as I think it would be cool to have my thesis be more interactive.

Is there any recommendation for whether I should use leanblueprint or verso?

[Alex Brodbelt]

For context it is only me working on the formalization of 12.7 Algebra of FLT (Classification of finite subgroups of $\textrm{PGL}_2(\overline{\mathbb{F}_p})$).
The creation of this "blueprint" is more for presenting the formalization in a way that presents the informal alongside the formal, alongside comments on decisions made, some of the mathematics and so forth.

[Kevin Buzzard]

FWIW I've been encouraging my Masters students to use Blueprint, because their projects are being marked by people who don't know Lean but who can make sense of a web page full of LaTeX and also of a blueprint graph.

[Alex Brodbelt]

Ok cool! I think I will use blueprint then, I think it would be a nice way to bring everything together. Thanks Kevin

[Ruben Van de Velde]

Why do these people not know lean :thinking:

[Alex Brodbelt]

these people don't know lean yet hehe

[Kevin Buzzard]

Because the algorithm for the markers of projects I supervise is "some committee chooses a random staff member who they believe is competent in the mathematics involved" and I can't change that.

[Alex Brodbelt]

When I tried setting up the blueprint, I ran into issues with doc-gen4 and when I tried to solve it by creating a docbuild folder and its suitable lakefile.toml. But when I ran lake update doc-gen4 it deleted my whole local project (everything is fine as it is on github and simply cloned it back) but it would be nice if I could be pointed to a thread that is useful for setting up the blueprint :sweat_smile:

[Alex Brodbelt]

Kevin Buzzard said:

Because the algorithm for the markers of projects I supervise is "some committee chooses a random staff member who they believe is competent in the mathematics involved" and I can't change that.

Thankfully my supervisor is pulling some threads so there is a higher chance the second marker will be aware of lean and the nature of such a project. :praise:

[Alex Brodbelt]

uh_oh.png

[Alex Brodbelt]

I am aware of other threads where problems with leanblueprint have been mentioned. I'll keep trying to get it up and running on my own, in the meantime if there is any advice on how to set it up I will gladly take such advice :-)

[Yaël Dillies]

(#general would be a better fit than #lean4 for verso- or leanblueprint-related queries)

[Alex Brodbelt]

Hi!

I am trying to set up leanblueprint for my project classifying finite subgroups of $\textrm{PGL}_2(\overline{\mathbb{F}_p})$ which will constitute my thesis and the formalization of 12.7 Algebra in FLT.

I followed the instructions for setting up leanblueprint (https://github.com/PatrickMassot/leanblueprint?tab=readme-ov-file): downloaded prerequisites and then ran leanblueprint new and modified GitHub actions to what I figured was appropriate.

But it seems the lean server can not start as there seems to be a problem with doc-gen4

stderr:
error: dependency '«doc-gen4»' not in manifest; use `lake update «doc-gen4»` to add it
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

after this I looked at FLT repo to see what leanblueprint set up looks like and checked doc-gen4repo to see if any instructions where useful and saw that I was missing docbuild/lakefile.toml so created this folder and an appropriate file.

After this, I ran MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4 in both the project directory and the docbuilddirectory.

The first yielded the following error:

alex-brodbelt@alex-brodbelt-ThinkPad-X1-Carbon-Gen-12:~/Desktop/Projects/Lean/Dissertation/ClassificationOfFiniteSubgroupsOfPGL/docbuild$ MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4
info: docbuild: no previous manifest, creating one from scratch
trace: ././../.lake/packages/doc-gen4> git fetch --tags --force origin
error: ././../.lake/packages/doc-gen4/lakefile.lean:134:4: error: unknown identifier 'addTrace'
error: ././../.lake/packages/doc-gen4/lakefile.lean:135:4: error: unknown identifier 'addTrace'
error: ././../.lake/packages/doc-gen4/lakefile.lean:138:4: error: unknown identifier 'addTrace'
error: ././../.lake/packages/doc-gen4/lakefile.lean:139:4: error: unknown identifier 'addTrace'
error: ././../.lake/packages/doc-gen4/lakefile.lean:142:4: error: unknown identifier 'addTrace'
error: ././../.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.BuildJob.mapM'
  exeJob
has type
  BuildJob FilePath
error: ././../.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.Job.mapM'
  exeJob
has type
  Job (FilePath × BuildTrace)
error: ././../.lake/packages/doc-gen4/lakefile.lean:144:2: error: invalid field 'mapM', the environment does not contain 'Lake.JobCore.mapM'
  exeJob
has type
  JobCore (JobTask (FilePath × BuildTrace))
error: ././../.lake/packages/doc-gen4/lakefile.lean:156:22: error: failed to synthesize
  FamilyOut CustomData (bibPrepass.pkg, bibPrepass.name) ?m.7166
Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: ././../.lake/packages/doc-gen4/lakefile.lean:159:16: error: invalid field 'await', the environment does not contain 'Array.await'
  __do_lift✝
...

and then the latter where I ran MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4 within docbuild directory yielded the following error:

alex-brodbelt@alex-brodbelt-ThinkPad-X1-Carbon-Gen-12:~/Desktop/Projects/Lean/Dissertation/ClassificationOfFiniteSubgroupsOfPGL/docbuild$ lake update «doc-gen4»
info: docbuild: no previous manifest, creating one from scratch
trace: ././../.lake/packages/doc-gen4> git fetch --tags --force origin
error: ././../.lake/packages/doc-gen4/lakefile.lean:137:4: error: unknown identifier 'addTrace'
error: ././../.lake/packages/doc-gen4/lakefile.lean:138:4: error: unknown identifier 'addTrace'
error: ././../.lake/packages/doc-gen4/lakefile.lean:141:4: error: unknown identifier 'addTrace'
error: ././../.lake/packages/doc-gen4/lakefile.lean:142:4: error: unknown identifier 'addTrace'
error: ././../.lake/packages/doc-gen4/lakefile.lean:145:4: error: unknown identifier 'addTrace'
error: ././../.lake/packages/doc-gen4/lakefile.lean:147:2: error: invalid field 'mapM', the environment does not contain 'Lake.BuildJob.mapM'
  exeJob
has type
  BuildJob FilePath
error: ././../.lake/packages/doc-gen4/lakefile.lean:147:2: error: invalid field 'mapM', the environment does not contain 'Lake.Job.mapM'
  exeJob
has type
  Job (FilePath × BuildTrace)
error: ././../.lake/packages/doc-gen4/lakefile.lean:147:2: error: invalid field 'mapM', the environment does not contain 'Lake.JobCore.mapM'
  exeJob
has type

[Kim Morrison]

Giving textual repro instructions is more likely to get help than screenshots.

[Kim Morrison]

(i.e. tell us which of your repositories to clone, which commands to run, etc)

[Alex Brodbelt]

my next thought is to maybe to fiddle with lake-manifest.json but I am not confident in my ability to do this successfully.

[Alex Brodbelt]

These are the contents of lake-manifest.json:

{"version": "1.1.0",
 "packagesDir": ".lake/packages",
 "packages":
 [{"url": "https://github.com/leanprover-community/batteries",
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
   "rev": "dd6b1019b5cef990161bf3edfebeb6b0be78044a",
   "name": "batteries",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/quote4",
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
   "name": "Qq",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/aesop",
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
   "name": "aesop",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": true,
   "configFile": "lakefile.toml"},
  {"url": "https://github.com/leanprover-community/ProofWidgets4",
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
   "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
   "name": "proofwidgets",
   "manifestFile": "lake-manifest.json",
   "inputRev": "v0.0.43",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover/lean4-cli",
   "type": "git",
   "subDir": null,
   "scope": "leanprover",
   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
   "name": "Cli",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.toml"},
  {"url": "https://github.com/leanprover-community/import-graph",
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
   "name": "importGraph",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.toml"},
  {"url": "https://github.com/leanprover-community/LeanSearchClient",
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
   "name": "LeanSearchClient",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.toml"},
  {"url": "https://github.com/leanprover-community/mathlib4",
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
   "rev": "e3e46c381d49179c3818135c0a888bc69a958de3",
   "name": "mathlib",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": false,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/PatrickMassot/checkdecls.git",
   "type": "git",
   "subDir": null,
   "scope": "",
   "rev": "75d7aea6c81efeb68701164edaaa9116f06b91ba",
   "name": "checkdecls",
   "manifestFile": "lake-manifest.json",
   "inputRev": null,
   "inherited": false,
   "configFile": "lakefile.lean"}],
 "name": "ClassificationOfSubgroups",
 "lakeDir": ".lake"}

[Kim Morrison]

Don't touch lake-manifest.json, it is automatically generated.

[Kim Morrison]

You haven't given us a repro.

[Kim Morrison]

I want something like:

git clone XXX
cd XXX
git checkout YYYY
lake update

that I can run independently.

[Notification Bot]

This topic was moved here from #lean4 > setting up leanblueprint by Patrick Massot.

[Patrick Massot]

The error messages very much look like a Lean version mismatch (maybe the project and doc-gen try to use different versions of Lean).

[Patrick Massot]

And please don’t double-post like this. This makes people waste time by answering questions that are already handled elsewhere.

[Patrick Massot]

For other confused people: this thread is a duplicate of #general > issues setting up leanblueprint

[Notification Bot]

15 messages were moved here from #general > setting up leanblueprint by Ruben Van de Velde.

[Alex Brodbelt]

Patrick Massot said:

And please don’t double-post like this. This makes people waste time by answering questions that are already handled elsewhere.

I believe I am not allowed to move messages, I was going to do so, but it says I don't have permission to move messages. Sorry about that.

[Patrick Massot]

Don’t worry too much about this, but next time you should wait for someone to do the move instead of double posting.

[Alex Brodbelt]

Kim Morrison said:

I want something like:

git clone XXX
cd XXX
git checkout YYYY
lake update

that I can run independently.

My repository can be found at https://github.com/AlexBrodbelt/ClassificationOfFiniteSubgroupsOfPGL:

I ran the following commands:

Entered directory where I have a python venv and want my project to be

git clone git@github.com:AlexBrodbelt/ClassificationOfFiniteSubgroupsOfPGL.git

cd ClassificationOfFiniteSubgroupsOfPGL

Activated python venv containing leanblueprint and other prerequisites (I am aware the naming might not have been a good idea...)

source .leanblueprint/bin/activate

leanblueprint new

Magic started to happen and it looked good, I was asked questions and used the default answers as they seemed reasonable which eventually pushed the new files to remote.

Got the error: dependency '«doc-gen4»' not in manifest; use lake update «doc-gen4» to add it

Created docbuild folder with lakefile.toml and copied contents of corresponding FLT file and changed the
name to ClassificationOfSubgroups (not savy with commands yet)

lake update «doc-gen4»

Got the first error above, so then tried instructions of doc-gen4

cd docbuild

lake update «doc-gen4»

Got the second error above

[Alex Brodbelt]

Is this more useful Kim Morrison ? (I don't mean to alert, not sure how to mention without alerting. Edit: does not alert now)

[Patrick Massot]

https://zulip.com/help/mention-a-user-or-group#silently-mention-a-user

[Alex Brodbelt]

Patrick Massot said:

The error messages very much look like a Lean version mismatch (maybe the project and doc-gen try to use different versions of Lean).

How can I fix the mismatch?

I've tried lake update and after peeking at #general > Updating to 4.15.0 tried to simulate some things as I get a similar error, but have had no luck so far...

[Patrick Massot]

We can’t help you more if you don’t help us helping you, as explained by Kim yesterday.

[Alex Brodbelt]

What else should I do to make it easier to help me? I think I provided all the commands I ran. I'll add the link to the github repository if that's helpful too.

The last message from me, was me trying some things in the meantime but not convinced they would work.

[Patrick Massot]

Oh sorry, I missed that message. Because it is long, Zulip is folding it and I wasn’t seeing the relevant part.

[Patrick Massot]

I don’t have time now, but I’ll come back to it if nobody does it first.

[Alex Brodbelt]

OK, I managed to update lean and that helps (thanks Patrick!), but still I am having trouble with doc-gen (as GitHub actions states). I will keep trying and will update where I am at.

[Alex Brodbelt]

Ok, so I have updated essentially everything.

-Updated Lean to v4.17.0-rc1
-Updated elan to 4.0.0
-Updated lake to 5.0.0-93d4ae6
-Updated mathlib dependencies now on version 4a69dc8b998d4bedb9541bc4dd45685be03f5fd5

Now lake exe cache get and lake buildwork beautifully.

I might have overcooked it though, I ran:

(
Assuming the following has already been done:

git clone git@github.com:AlexBrodbelt/ClassificationOfFiniteSubgroupsOfPGL.git

cd ClassificationOfFiniteSubgroupsOfPGL

)

cd docbuild

lake update doc-gen4

This generates a lake file within docbuild (which I guess should not surprise me), but is this necessary for the blueprint to function correctly once I push to the remote repo?

[Alex Brodbelt]

It seems redundant considering the same folders are within the larger .lake file that the maths project itself uses. But I do not know how leanblueprint works.

[Alex Brodbelt]

GOT IT WORKING! very very exciting.

Is there a way to preview the LaTeX without needing to push and wait a few minutes for it to build? What is the typical workflow like?

[Yaël Dillies]

Yes, you can build everything locally. #leanblueprint should have instructions

[Yaël Dillies]

Oh, no linkifier. I mean https://github.com/PatrickMassot/leanblueprint

[Alex Brodbelt]

Cool! thanks

[Kevin Buzzard]

leanblueprint web then leanblueprint serve

[Alex Brodbelt]

Aha yes, this is exactly what I need

[Alex Brodbelt]

Is there a way to embed the lean code in the blueprint? My supervisor thinks the format:

• Informal statement
• Formal statement in lean
• Informal proof
• Formal proof in lean
• Comments on formalization

would be a good way to present a lean project, as it would serve as a Rosetta stone for how to work with this particular part of mathlib and this area of mathematics.

In particular, it would be a good way to introduce lean to non-lean users. I think I agree with this sentiment but I am aware of other threads were Patrick and Kevin think it is best to separate the presentation of the informal maths from the formal maths, and was wondering why this is so?

Ultimately, I think I might have to use the minted package as Johan mentions but just thought I would poke this comment/question out here on zulip. Maybe someone has some interesting thoughts?