leanblueprint command line tool

Stream: general

[Patrick Massot]

I am looking for beta-tester for the new Lean blueprint command line tool. Documentation is available at https://github.com/PatrickMassot/leanblueprint/blob/client/README.md.

The short version is: in your favorite Lean project hosted on GitHub, you will be able to:

• click one button on GitHub to enable GitHub pages
• run leanblueprint new and answer a couple of question (accepting all default answers should be fine)
• run git push
• Wait for a couple of minutes (depending on the size of your project)
• Enjoy your API doc, blueprint pdf and blueprint web pages on github.io

I tested it on a project stub but I wouldn’t be surprised if there are bugs, especially with the continuous integration setup. That’s why I didn’t push to pypi yet.

[Patrick Massot]

Note that leanblueprint new will add a couple of lines to your lakefile.lean. However it won’t edit your existing GitHub workflow files, it will create a new one.

[Patrick Massot]

Of course all this requires a sane python setup.

[Antoine Chambert-Loir]

(9:20) pro-acl > pip install git+https://github.com/PatrickMassot/leanblueprint.git@client

Successfully built leanblueprint
Failed to build pygraphviz
Installing collected packages: smmap, pygraphviz, mdurl, plasTeX, markdown-it-py, gitdb, rich, plastexshowmore, plastexdepgraph, GitPython, rich-click, leanblueprint
  Running setup.py install for pygraphviz ... error

Do you have an idea of what I could do?

[Antoine Chambert-Loir]

(I tried what is told on pygraphviz home page and it worked.)

[Antoine Chambert-Loir]

Now, lualatex web tells me that blueprint.sty is missing. (And leanblueprint pdf failed as well.)

[Kim Morrison]

Patrick Massot said:

Note that leanproject new will add a couple of lines to your lakefile.lean. However it won’t edit your existing GitHub workflow files, it will create a new one.

leanproject new here is presumably a Freudian slip of some kind. :-)

[Patrick Massot]

Muscle memory...

[Patrick Massot]

Antoine, could you list the content of the blueprint/src folder?

[Patrick Massot]

Sorry I read @Antoine Chambert-Loir ’s message too quickly. There is no issue on leanblueprint side, you simply tried to compile the web version using lualatex, which is bound to fail. This does not explain why leanblueprint pdf failed, I will need more information here. Could you try running latexmk directly in the blueprint/src folder?

[Patrick Massot]

@Sébastien Gouëzel and @Rémy Degenne I’d be especially interested in test on Windows. Note your still need to be able to install graphviz. But everything else is meant to be easier.

[Julian Berman]

@Antoine Chambert-Loir can you show the result of pip wheel -vv pygraphviz

[Julian Berman]

Patrick I'm going to try to help give you a single binary (a thing someone can download and just run which has all the dependencies), but in case I fail at it or get distracted make believe I didn't say that till later when I try to send a PR. (EDIT: Ugh, PyApp is less ready than I'd hoped, so I've put this on hold, though I think if I try again I'll get further.)

[Antoine Chambert-Loir]

Julian Berman said:

Antoine Chambert-Loir can you show the result of pip wheel -vv pygraphviz

It's too long for zulip, so I sent it to you by email.

[Antoine Chambert-Loir]

Patrick Massot said:

Antoine, could you list the content of the blueprint/src folder?

(15:17) pro-acl > ls blueprint/src
content.tex       extra_styles.css  latexmkrc         plastex.cfg
print.tex         texput.log        web.log           web.paux
web.tex

[Antoine Chambert-Loir]

Patrick Massot said:

Sorry I read Antoine Chambert-Loir ’s message too quickly. There is no issue on leanblueprint side, you simply tried to compile the web version using lualatex, which is bound to fail. This does not explain why leanblueprint pdf failed, I will need more information here. Could you try running latexmk directly in the blueprint/src folder?

! Package fontspec Error: The font "Latin Modern Math" cannot be found.

For immediate help type H <return>.
 ...

l.26 \setmathfont
                 [range=\varnothing]{Asana-Math.otf}

[Julian Berman]

@Antoine Chambert-Loir oh, so that worked? You now have a .whl file from that output. But your output above said Running setup.py install for pygraphviz ... error which means it failed -- does the original pip install succeed now?

[Julian Berman]

Oh sorry, I too misunderstood the end of what you said, that after you ran what's on the pygraphviz page it did work. OK.

[Patrick Massot]

Thanks Antoine. So this issue has nothing to do with Lean or Python, your LaTeX install cannot find the Latin modern Math font.

[Patrick Massot]

I have no idea how you managed to install LaTeX and still not have this font. But it suggests I should remove this from the template and let people use old fonts.

[Antoine Chambert-Loir]

Julian Berman said:

Oh sorry, I too misunderstood the end of what you said, that after you ran what's on the pygraphviz page it did work. OK.

Yes, after the pip command suggested by @Patrick Massot failed, I went to the pygraphviz home page which suggested another way of installing it.

[Patrick Massot]

Actually I realized I wrote in the README that you can use pdflatex if you are really nostalgic, but this is a lie.

[Patrick Massot]

I just pushed a commit removing all font selection commands from the template.

[Antoine Chambert-Loir]

Patrick Massot said:

Thanks Antoine. So this issue has nothing to do with Lean or Python, your LaTeX install cannot find the Latin modern Math font.

I understand that issue, but since I have a TeXLive 2023 install, with, in principle, all of it, I don't see how my LaTeX install could miss it.

[Patrick Massot]

And I removed any mention of pdflatex in the blueprint. There is no reason to mention this program in 2024 anyway.

[Antoine Chambert-Loir]

Patrick Massot said:

I have no idea how you managed to install LaTeX and still not have this font. But it suggests I should remove this from the template and let people use old fonts.

MacTeX install

[Antoine Chambert-Loir]

Patrick Massot said:

And I removed any mention of pdflatex in the blueprint. There is no reason to mention this program in 2024 anyway.

really? why not?

[Patrick Massot]

I guess google will tell you how to install this font if you really want it. But the goal of the leanblueprint command line tool is to make it easy to start a blueprint. Using this font is not a core requirement so I want to remove this friction point.

[Patrick Massot]

pdflatex is very unicode unfriendly. It has been replaced by xelatex and lualatex a long time ago.

[Antoine Chambert-Loir]

Well, that looks like an overstatement. For example, arXiv does not accept lualatex.

[Patrick Massot]

arXiv is very much stuck in the 90’s, but there are good reasons for this. The challenge of being able to compile everything that was ever submitted there is huge. They still want to move on, but it’s very non-trivial.

[Patrick Massot]

I forgot to mention one important thing. When I created the blueprint plugin for the sphere eversion project, I did not setup any continuous integration for it, because I hate setting up CI. The blueprint was compiled locally and the result was pushed to the Lean repo. So the CI template that is now used by leanblueprint is based on the work of other people. I don’t know the full story but I think @Yakov Pechersky is the pioneer who did this work for the Liquid tensor experiment. I’ll mention his name in the README, but I’d be happy to mention other names if someone knows the full story. I started my work here with the PFR version by @Yaël Dillies. Yaël, did you copy a CI file from somewhere else or did you start from scratch?

[Yakov Pechersky]

Ben Toner did a ton of work too!

[Patrick Massot]

This is the other name that I had in mind but somehow https://github.com/leanprover-community/liquid/commits/master/.github/workflows shows only one commit, so I got confused.

[Yaël Dillies]

I copied it from LeanAPAP, which inherited its CI setup from Con(NF), which @Sky Wilshaw and I set up together.

[Yaël Dillies]

In the port to Lean 4, it also acquired a few changes due to @Utensil Song

[Yaël Dillies]

In short: it's mostly Sky's original doing + a constant need on my part for more advanced features + Utensil's improvements during the port

[Patrick Massot]

Thanks. I pushed an updated README.

[Patrick Massot]

And I can add more later if more names appear.

[Patrick Massot]

By the way, contributions to that file are very welcome. I spend a lot of time randomly editing that file until it works, and I now hate CI setup even more.

[Patrick Massot]

One thing that would have made everything a lot easier is having a better docker image with both TeXlive and Lean (see this thread).

[Patrick Massot]

The docker image used by PFR and my template is based on Alpine Linux that is not supported by elan.

[Patrick Massot]

The nice thing to do would simply be to create a docker image with every dependency installed (TeXlive, elan and graphviz). But I have no idea how to do that and I cannot spend one more week learning about docker.

[Sky Wilshaw]

I did that for Con(NF), but it actually ended up being quite inconvenient. In particular, elan is fast to download+install and TeXlive is not. So if we run from a Docker image, we have to install TeXlive even if the build fails. In my use case, I wanted the build to fail early if I had any errors.

[Sky Wilshaw]

In any case, you might be able to use my old Dockerfile for inspiration.

[Patrick Massot]

I see. Indeed pulling the Docker image already takes quite a bit of time.

[Patrick Massot]

However this is relevant only for very small projects. Building the Lean project should very quickly become the bottleneck.

[Sky Wilshaw]

I actually experienced a halving of CI time once I removed leanblueprint and its dependencies. TeXlive really takes a while to install, and the TeX engine itself was quite slow. For context, Con(NF) is around 10k LOC.

[Patrick Massot]

What do you mean by “TeXlive really takes a while to install”? Do you mean pulling a docker image where it is installed or installing it in a default GitHub CI image that does not provide it?

[Sky Wilshaw]

Either of them. The bottleneck is network transfer speed.

[Sky Wilshaw]

They both take around an additional 2min30 in my experience when adding TeXlive.

[Sky Wilshaw]

For projects as big as mathlib, 2min30 is not much, but in my case it was enough to be concerned about.

[Patrick Massot]

Yes, 2 minutes is what I saw where  I struggled with this. Yesterday it indeed drove me crazy, but I’m not too worried in real world conditions. And there is nothing we can do anyway. We need TeX for the pdf version.

[Sky Wilshaw]

It's probably possible to use a TeX distribution that doesn't download all the packages in advance, like Tectonic.

[Sky Wilshaw]

It uses XeLaTeX/TeXlive for everything under the hood, so would hopefully be compatible with whatever you're already using.

[Patrick Massot]

This sounds like an interesting thing to try.

[Patrick Massot]

Contributions are welcome :wink:

[Patrick Massot]

It’s all about modifying https://github.com/PatrickMassot/leanblueprint/blob/client/leanblueprint/templates/blueprint.yml

[Utensil Song]

I'm still recovering from a sickness since the new year and enjoying much less Lean time. leanblueprint CLI is something I wished for and will try it once I have some Lean time, for one, I haven't checked if it has everything I wished for and described in PatrickMassot/leanblueprint#6 yet.

[Utensil Song]

As for Tectonic, personally I've been using it here and the correspoding invoke python script here. There are a few things to note, like leanblueprint depends on kpsewhich via plastex, which requires a minimal TeX installation. Plastex also needs the bbl file generated during PDF generation for the Bibliography and thus the --keep-intermediates option of Tectonic.

In general, Tectonic has good compatibility with complicated LaTeX files as it reuse the LaTeX packages, only in an incremental way, but there are some caveats to pay attention to here and there, I can't recall all of them, but at least it doesn't play very well with minted and similar packages that requires executing external commands. That said, Tectonic alone works sufficiently well but it plays less nice with plastex which is the backbone of leanblueprint and assumes the existence of some parts of the LaTeX installation.

During pfr projects, I was polishing the CI process using the old fashioned TeXLive way and my own workflow also moved back to the old fashioned TeXLive way as a testbed and also because of a few caveats of Tectonic, for one, I wanted to include the generated GraphViz/dot file (of the dep_graph) in the PDF, but I had some trouble with Tectonic but not TeXLive.

[Patrick Massot]

I think it does everything mentioned in that issue except the changes to the produced pdf.

[Patrick Massot]

Thanks for the information about Tectonic. It doesn't seem worth the trouble.

[Rémy Degenne]

@Patrick Massot I finally tried the leanblueprint comand line tool. I am trying it on windows. I installed leanblueprint with pip, created a github repository, created a lean project, linked it to the repository and pushed, and finally activated page deployment.
Then when I use leanblueprint new in my project folder (and accept all the default answers), I get this error:

'charmap' codec can't encode character '\u202f' in position 18: character maps to <undefined>

Any idea of what could be wrong?

[Rémy Degenne]

That character is apparently Narrow No-Break Space, and it definitely does not appear in the project name or path.

[Rémy Degenne]

And to be more complete, here is the full output of leanproject new:

$ leanblueprint new

Welcome to Lean blueprint

We will now ask some questions to configure your blueprint. All answers can ce
changed later by editing either the plastex.cfg file or the tex files.

General information about the project
Project title (My formalization project):
Lean library name [TestingLowerBounds] (½TestingLowerBounds):
Author (use \and to separate authors if needed) (RemyDegenne):
Url of github repository (https://github.com/RemyDegenne/testing-lower-bounds):
Url of project website (https://RemyDegenne.github.io/testing-lower-bounds):
'charmap' codec can't encode character '\u202f' in position 18: character maps to <undefined>

[Patrick Massot]

Thanks for testing this @Rémy Degenne. I pushed a fix

[Patrick Massot]

I have no idea why your computer doesn’t like this space but it was a typo anyway.

[Patrick Massot]

That sometimes happen because thin non-breakable space is mapped to shift-space on the keyboard layout I use and sometimes when typing fast they get inserted in the wrong place.

[Rémy Degenne]

Thanks! A new, similar error:

$ leanblueprint new

Welcome to Lean blueprint

We will now ask some questions to configure your blueprint. All answers can ce
changed later by editing either the plastex.cfg file or the tex files.

General information about the project
Project title (My formalization project): Testing lower bounds
Lean library name [TestingLowerBounds] (½TestingLowerBounds): TestingLowerBounds
Author (use \and to separate authors if needed) (RemyDegenne): Rémy Degenne
Url of github repository (https://github.com/RemyDegenne/testing-lower-bounds):
Url of project website (https://RemyDegenne.github.io/testing-lower-bounds):
Url of project API documentation
(https://RemyDegenne.github.io/testing-lower-bounds/docs):

LaTeX settings for the pdf version
LaTeX document class (report):
LaTeX paper (a4paper):

LaTeX settings for the web version
Show buttons allowing to show or hide all proofs [y/n] (y):
Table of contents depth (3): 2
Split file level (0 means each chapter gets a file, 1 means the same for
sections etc.) (0):
Per html file local table of contents depth (0 means there will be no local
table of contents) (0):

Configuration completed
Proceed with blueprint creation? [y/n]: y
content.tex
extra_styles.css
latexmkrc
plastex.cfg
print.tex
web.tex

'charmap' codec can't encode character '\U0001f389' in position 61: character maps to <undefined>

[Rémy Degenne]

This is the party popper character :tada:

[Patrick Massot]

Something is really wrong with your python installation.

[Patrick Massot]

Are you running python 2?

[Patrick Massot]

That one is not a typo.

[Rémy Degenne]

3.8

[Rémy Degenne]

I can try it in a new environment instead of with my global python and see if I get the same issue

[Patrick Massot]

It does not even appear in the source code, it is produced by the rich library. In the source code it appears as :tada:.

[Patrick Massot]

Could you try in another shell?

[Patrick Massot]

I’m curious about this but I will remove it anyway. Since emoji is not essential and there will be other people using broken shells.

[Rémy Degenne]

This was in Git Bash. I just tried it in anaconda prompt from miniconda3 (also in a fresh environment) and everything worked perfectly

[Rémy Degenne]

Well, I got to the end of the leanblueprint new command. Now CI complains when I push because I have unexpected tokens in lakefile.lean, but that's an other error.

meta if get_config? env = some "dev" then
require �doc-gen4� from git
  "https://github.com/leanprover/doc-gen4" @ "main"

[Patrick Massot]

I really don’t know how you can have the patience to use Windows.

[Patrick Massot]

But I pushed a new commit trying to work around those issues.

[Rémy Degenne]

You asked me to test it on Windows :)
Otherwise I would have done it on linux (I learned my lesson last time).

[Patrick Massot]

I mean I don’t know how anyone can have the patience to use Windows. I am very grateful that you are doing this test on Windows.

[Patrick Massot]

For years the answer to this question was always the same: people had Windows because of video games. But this is no longer a criterion now that Steam and Proton exist.

[Rémy Degenne]

Summary of my most recent attempt, with references to the commits here: https://github.com/RemyDegenne/testing-lower-bounds/commits/master/

• leanproject new worked
• I pushed the automatically generated commit (commit "Setup blueprint"). CI failed in build and told me to run lake update checkdecls
• I did that and pushed (commit "lake update checkdecls"). CI failed and told me to run lake update «doc-gen4»
• I did that but it did absolutely nothing. I remembered my problems with doc-gen from last time I tried to use it, went to the doc-gen page and read that I should use lake -R -Kenv=dev update
• I ran that command and pushed (commit "lake -R -Kenv=dev update"). CI failed because of an unknown target «TestingLowerBounds.
• After a while, I discovered that the project name was wrong in .github/workflows/blueprint.yml: it was written «TestingLowerBounds instead of TestingLowerBounds. I fixed it (commits "fix workflow?" and "fix workflow again") and the build step succedded in CI.

Now CI fails at the build blueprint step with error LaTeX Error: File 'macros/common.tex' not found.: https://github.com/RemyDegenne/testing-lower-bounds/actions/runs/8010524168/job/21881676723

[Rémy Degenne]

I created manually macros/common.tex and macros/print.tex and CI succeeded.

[Patrick Massot]

All of this is horribly wrong. None of those steps should be necessary.

[Patrick Massot]

I will clone your repo and try to reproduce.

[Rémy Degenne]

And I'll uninstall leanblueprint, start in a new environment, make a completely new project, go to the step where I push the "Setup blueprint" commit and see what I get.

[Patrick Massot]

For instance you can see from https://github.com/RemyDegenne/testing-lower-bounds/commit/f890060c7e1f5871e2bab2c3253f73ad7e8828e3#diff-4e2751aec1a84ced68388517cb6f54720d3316f73ea035b8c559d9e028af0581R29 that leanblueprint failed to extract the lib name from the lakefile.

[Patrick Massot]

I fixed this bug but I really don’t understand why I didn’t hit it in my tests.

[Patrick Massot]

However I have no clue about why the macros files were not created on your side. I cannot reproduce that.

[Rémy Degenne]

I just tested with a new repository (before your fix I guess) and I have the same errors: project name and no macros/... files.

[Patrick Massot]

I have an idea, hold on.

[Patrick Massot]

Could you try again?

[Rémy Degenne]

https://github.com/RemyDegenne/lbp-test

[Rémy Degenne]

The project name looks good. The macros files are there. Let's wait for CI.

[Rémy Degenne]

Run ~/.elan/bin/lake -Kenv=dev build LbpTest
error: dependency 'checkdecls' not in manifest; use `lake update checkdecls` to add it
Error: Process completed with exit code 1.

[Patrick Massot]

CI failed

[Patrick Massot]

that stuff is so non-deterministic...

[Patrick Massot]

Everything worked two weeks ago.

[Patrick Massot]

The following bit is also puzzling:

Run curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0
  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0
  shell: /usr/bin/bash -e {0}
info: downloading installer
info: Version 3.1.0 of elan is available! Use `elan self update` to update.

How can elan install itself and immediately ask for an upgrade?

[Patrick Massot]

I think I now why it was working in my test: I guess I had not lake manifest all in my test project before pushing the blueprint creation commit.

[Patrick Massot]

It almost works in your project now but it seems you forgot to enable GitHub pages.

[Rémy Degenne]

Yes I just did that and restarted CI

[Patrick Massot]

Patrick Massot said:

The following bit is also puzzling:

Run curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0
  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0
  shell: /usr/bin/bash -e {0}
info: downloading installer
info: Version 3.1.0 of elan is available! Use `elan self update` to update.

How can elan install itself and immediately ask for an upgrade?

@Sebastian Ullrich do you have any idea what is happening above? This is in CI  so we don’t have access to the machine to investigate.

[Patrick Massot]

In the mean time I modified the CI template.

[Rémy Degenne]

Rémy Degenne said:

Yes I just did that and restarted CI

Success.

[Patrick Massot]

I hope didn’t crash your windows with that emoji reaction…

[Rémy Degenne]

The fact that there is no index.html file is expected? It's something I have to do myself in my project?

[Rémy Degenne]

This is a 404: https://remydegenne.github.io/lbp-test/
But this is fine: https://remydegenne.github.io/lbp-test/docs/

[Patrick Massot]

Yes, this is expected, the main web page of your project is outside the scope of this tool.

[Patrick Massot]

https://remydegenne.github.io/lbp-test/blueprint/ is there.

[Patrick Massot]

I could offer the option of creating a minimal Jekyll site if people want this.

[Rémy Degenne]

In summary that last attempt worked, except that I had to do lake -R -Kenv=dev update once after the leanblueprint new step.

[Rémy Degenne]

Patrick Massot said:

I could offer the option of creating a minimal Jekyll site if people want this.

That would be very nice.

[Patrick Massot]

Clearly this has also been a popular copy-paste target in the community.

[Patrick Massot]

But it’s not systematic. For instance LTE and FLT-regular have no home page.

[Patrick Massot]

About the lake update command, I added it in CI but it would also make sense to run it locally after creating the blueprint if people want to check declarations locally.

[Patrick Massot]

The only thing that worries me is that the script would fail if you want to create the blueprint but do not have Lean installed. I don’t know whether this is a problem.

[Rémy Degenne]

Anyway thanks a lot for that new blueprint setup tool! It is very convenient.

[Patrick Massot]

I guess I could try and continue even if this command fails.

[Patrick Massot]

Thank you very for testing it! I worked a lot on it and I was pretty frustrated to see nobody testing it.

[Patrick Massot]

Patrick Massot said:

Sebastian Ullrich do you have any idea what is happening above? This is in CI  so we don’t have access to the machine to investigate.

Thanks for the fix @Sebastian Ullrich !

[Sebastian Ullrich]

Yeah, I don't know how that one escaped my manual testing. Unfortunately, people who already installed/updated to elan 3.1.0 (i.e. in the last three days) may have to re-run the installer to update to the fixed 3.1.1

[Patrick Massot]

Hopefully there are not so many people. But we were lucky that this blueprint discussion got us looking closely at CI logs featuring a fresh install of elan.

[Sébastien Gouëzel]

I have finally some time to test it (on my fork of PFR), and I'll report as things go. Only hiccup for now:

Lean library name [PFR] (PFR): PFR_fork

wasn't accepted, apparently I have no choice here: I got the answer (in red)

Please select one of the available options

and the only choice that works as far as I can tell is PFR.

[Sébastien Gouëzel]

Second hiccup: after a phase of configuration, downloading mathlib and everything, I get

Modify lakefile to allow building the documentation on GitHub? [y/n] (y):
Ok, lakefile is edited.
Configure continuous integration to compile blueprint? [y/n] (y):
GitHub workflow file created at C:\Users\Sebastien\Desktop\pfr\.github\workflows\blueprint.yml

Commit to git repository? [y/n]: y
Commit message (Setup blueprint):
Invalid Type: WindowsPath('C:/Users/Sebastien/Desktop/pfr/blueprint')

[Sébastien Gouëzel]

(the path is the right one, and there are no weird spaces in it that could spoil anything)

[Sébastien Gouëzel]

(and nothing was commited to the repository yet)

[Michael Rothgang]

Patrick Massot said:

Thank you very for testing it! I worked a lot on it and I was pretty frustrated to see nobody testing it.

For the record: my long list of Lean-related things I want to try includes testing this new tool by trying to port the sphere-eversion blueprint to the new style. But at the moment, finishing my PhD thesis takes priority. :-)

[Patrick Massot]

The Lean library name seems correct to me. Do you really have a Lean library whose lake name is PFR_fork?

[Patrick Massot]

I should probably not display this question when I find only one line in the lake file.

[Patrick Massot]

The WindowsPath thing is more worrying and I really don’t understand why it’s an issue for you but not for Rémy.

[Patrick Massot]

Michael, please work on your thesis. I’m already very worried about what will happen the next time I’ll see Chris.

[Rémy Degenne]

I don't have time to test today but if you identify some things that you would like me to try later (to find out the differences between my setup and the installation of Sébastien, or anything else), I can do that tomorrow.

[Sébastien Gouëzel]

Patrick Massot said:

The Lean library name seems correct to me. Do you really have a Lean library whose lake name is PFR_fork?

No, the name is correct. I understood the question as "do you want to change the current name of the Lean library to something else?", since otherwise I couldn't see the point of the question.

[Sébastien Gouëzel]

Patrick Massot said:

The WindowsPath thing is more worrying and I really don’t understand why it’s an issue for you but not for Rémy.

If you have troubleshooting instructions (to get a traceback or something), just tell me. I'm on Python 3.7 by the way, I don't know if it can make a difference.

[Patrick Massot]

There is a point only if your project have several libs, so I will remove the question when there is only one lib.

[Patrick Massot]

About the path error, could you try running leanblueprint with the --debug option?

[Sébastien Gouëzel]

Sure. It gives me the following trace:

Traceback (most recent call last):
  File "c:\program files\python37\lib\runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "c:\program files\python37\lib\runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "C:\Users\Sebastien\AppData\Roaming\Python\Python37\Scripts\leanblueprint.exe\__main__.py", line 7, in <module>
  File "C:\Users\Sebastien\AppData\Roaming\Python\Python37\site-packages\leanblueprint\client.py", line 417, in safe_cli    handle_exception(err, str(err))
  File "C:\Users\Sebastien\AppData\Roaming\Python\Python37\site-packages\leanblueprint\client.py", line 74, in handle_exception
    raise exc
  File "C:\Users\Sebastien\AppData\Roaming\Python\Python37\site-packages\leanblueprint\client.py", line 415, in safe_cli    cli()  # pylint: disable=no-value-for-parameter
  File "c:\program files\python37\lib\site-packages\click\core.py", line 764, in __call__
    return self.main(*args, **kwargs)
  File "C:\Users\Sebastien\AppData\Roaming\Python\Python37\site-packages\rich_click\rich_command.py", line 126, in main
    rv = self.invoke(ctx)
  File "c:\program files\python37\lib\site-packages\click\core.py", line 1137, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "c:\program files\python37\lib\site-packages\click\core.py", line 956, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "c:\program files\python37\lib\site-packages\click\core.py", line 555, in invoke
    return callback(*args, **kwargs)
  File "C:\Users\Sebastien\AppData\Roaming\Python\Python37\site-packages\leanblueprint\client.py", line 321, in new
    repo.index.add([out_dir, lakefile_path, manifest_path] + workflow_files)
  File "c:\program files\python37\lib\site-packages\git\index\base.py", line 734, in add
    paths, entries = self._preprocess_add_items(items)
  File "c:\program files\python37\lib\site-packages\git\index\base.py", line 580, in _preprocess_add_items
    raise TypeError("Invalid Type: %r" % item)
TypeError: Invalid Type: WindowsPath('C:/Users/Sebastien/Desktop/pfr/blueprint')

[Patrick Massot]

Ok so this issue is purely internal to the GitPython library.

[Patrick Massot]

And indeed the difference with Rémy is probably a version mismatch.

[Patrick Massot]

I will try some naive workaround.

[Patrick Massot]

I pushed a new version

[Sébastien Gouëzel]

I have fixed it by updating gitpython. The old version was 3.1.0, and by updating to the last version (3.1.42) the issue disappeared.

[Sébastien Gouëzel]

So the best fix is probably to bump the requirements.

[Patrick Massot]

Oh no

[Patrick Massot]

I wanted you to test with your old version

[Patrick Massot]

The changelog of GitPython is a list of links instead of a searchable flat page… I really wonder what they were thinking about…

[Sébastien Gouëzel]

I've reverted to gitpython 3.1.0, so I can test the new version (I have just tested that the current one is failing as it used to).

[Patrick Massot]

Thanks. I’m curious to see if it works. In the mean time I found the first version of gitpython with the fix is probably 3.1.28.

[Sébastien Gouëzel]

It doesn't work (if I'm testing the right version -- is there a way to see if I haven't screwed up?)

[Patrick Massot]

Let’s not waste more time with this, I will bump the requirement.

[Patrick Massot]

I pushed a new version reverting the attempted workaround and requiring gitpython at least 3.1.28

[Sébastien Gouëzel]

In fact your fix was working, and I had screwed up (I had to uninstall leanblueprint and install it again to update it, maybe because the version number was the same?). Anyway, bumping the requirements is probably a better solution.

[Sébastien Gouëzel]

(And you forgot to push the requirement on gitpython :-)

[Patrick Massot]

I think that everybody that wanted to test the new blueprint client did it, so this is now the official release version. You can now install it using pip from pypi instead of GitHub: pip install leanblueprint. The documentation can be found at https://pypi.org/project/leanblueprint/0.0.4/ which shows the README of the current release.

[Patrick Massot]

Note this release also includes the LaTeX macros to redefine the graph colors (see documentation).

[Sébastien Gouëzel]

Sébastien Gouëzel said:

(And you forgot to push the requirement on gitpython :-)

Did you bump the gitpython requirements?

[Patrick Massot]

Yes

[Rémy Degenne]

@Patrick Massot I have a issue (on both windows and linux) with the bibliography on the web version. leanblueprint pdf generates the bibliography just fine, but leanblueprint web complains about a missing web.bbl (I have the same bibliography tex code for both versions). I see that I indeed have a print.bbl but no web.bbl (and if I rename the print one to web.bbl then leanblueprint web works fine).

In your client.py file, I see that mk_pdf has two lines of code that have something to do with bbl, and mk_web does not have that code. Perhaps that's related?

[Rémy Degenne]

@Patrick Massot sorry to ping you again but I am not sure if you saw my last message above. That's not urgent at all though.

[Patrick Massot]

I’m sorry I didn’t answer. I saw it and created a GitHub issue, but this will need to wait a bit (at least past the ITP deadline).

[Utensil Song]

The issue created was PatrickMassot/leanblueprint#12

Some more context: this was solved in the previous inv tasks.py like this:

@task
def bp(ctx):
    cwd = os.getcwd()
    os.chdir(BP_DIR)
    run('mkdir -p print && cd src && xelatex --shell-escape -output-directory=../print print.tex')
    run('cd print && bibtex print.aux', env={'BIBINPUTS': '../src'})
    run('cd src && xelatex --shell-escape -output-directory=../print print.tex')
    run('cd src && xelatex --shell-escape -output-directory=../print print.tex')
    run('cp print/print.bbl src/web.bbl')
    os.chdir(cwd)

which runs LaTeX once, to generate metainfo for the bbl file, then uses bibtex to generate a print.bbl then copies it to web.bbl to be consumed by plastex.

For anyone using tectonic, this is done in a one-pass manner like this, but requires an extra --keep-intermediates to keep the bbl file:

@task
def bptt(ctx):
    """
    Build the blueprint PDF file and prepare src/web.bbl for task `web`
    """

    cwd = os.getcwd()
    os.chdir(BP_DIR)
    run('mkdir -p print && cd src && tectonic -Z shell-escape-cwd=. --keep-intermediates --outdir ../print print.tex')
    run('cp print/print.bbl src/web.bbl')
    os.chdir(cwd)

[Utensil Song]

While we are at Bibliography, there is a related issue that I reported as plastex/plastex#348 : Same author in Bibliography is rendered to to3em for style amsalpha etc. for HTML.

image.png

[Patrick Massot]

The bbl file issue should be fixed in the latest release.

[Rémy Degenne]

Great, thanks!

[Rémy Degenne]

After your change, leanblueprint pdf also generates a file web.bbl, and then leanblueprint web succeeds. So locally everything is fine. However when I push to the git repository CI does not perform the pdf step, the bbl file is not generated and there is no bibliography on the website.

The solution is obviously to push the web.bbl file to the git repository, but would it be possible to generate it automatically in the CI "build blueprint" step?

[Patrick Massot]

Oh yes, I forgot CI, sorry.

[Patrick Massot]

Actually I’m confused. CI should do the right thing already.

[Rémy Degenne]

I may or may not have forgotten to update the leanblueprint files on the repository...

[Rémy Degenne]

I actually have no idea. Should I update something in my repository to make it change its leanblueprint version?

[Rémy Degenne]

I think I see why you say it should do the right thing: apparently CI does leanblueprint pdf, contrary to what I was claiming.

pip install git+https://github.com/PatrickMassot/leanblueprint.git@client
leanblueprint pdf
mkdir docs
cp blueprint/print/print.pdf docs/blueprint.pdf
leanblueprint web

(and the answer to my last question seems to be no: CI will install the latest version)

[Rémy Degenne]

But I still don't get a bibliography unless I push web.bbl

[Patrick Massot]

Is this happening in a public repository?

[Rémy Degenne]

https://github.com/RemyDegenne/testing-lower-bounds

[Patrick Massot]

Ok, I understand. The workflow file still installs leanblueprint from the client branch that was my dev branch.

[Patrick Massot]

It means you created this blueprint during the testing phase of the client.

[Patrick Massot]

https://github.com/RemyDegenne/testing-lower-bounds/pull/1

[Rémy Degenne]

Thanks a lot!

[Sam van G]

Hello!
@María Inés de Frutos Fernández and I are installing Leanblueprint following the instructions here, but running the command pip install git+https://github.com/PatrickMassot/leanblueprint.git@client only gets us to version 0.0.3. Is this wanted behavior?
I was able to get version 0.0.6 (which appears to be the most recent) by doing pip install git+https://github.com/PatrickMassot/leanblueprint.git (so omitting the @client at the end).

[Rémy Degenne]

These instructions are outdated. pip install leanblueprint is the correct way to install.

[Richard Osborn]

For people on mac who want to install leanblueprint globally via pipx, you may need to set your environment variables so that pygraphviz can locate the graphviz installed by homebrew.

export CFLAGS="-I$(brew --prefix graphviz)/include/"
export LDFLAGS="-L$(brew --prefix graphviz)/lib/"
pipx install leanblueprint

[Patrick Massot]

If some other Mac user confirms this is useful then I could add it to the documentation.

[Utensil Song]

See also https://pygraphviz.github.io/documentation/stable/install.html#homebrew which is essentially the same thing but a little verbose and not for pipx.

[Patrick Massot]

Ok so I don’t need it if it’s already on pygraphviz website.

[Richard Osborn]

The issue is that pipx creates a new virtual environment for leanblueprint and installs pygraphviz in that environment. I found that setting CFLAGS and LDFLAGS was the only simple way of getting pipx to install pygraphviz cleanly.

[Rémy Degenne]

@Patrick Massot I noticed an issue with the doc on the blueprint at https://remydegenne.github.io/testing-lower-bounds/blueprint/sect0002.html .

I have a latex file that references lemmas in two lean files, which at some point were TestingLowerBounds/FDiv.lean and TestingLowerBound/CondFDiv.lean. I moved both files to a subfolder, such that they are now TestingLowerBounds/FDiv/Basic.lean and TestingLowerBounds/FDiv/CondFDiv.lean.
Now when I click a "LEAN" link in the blueprint that is supposed to send me to the FDiv/Basic file it works fine (for example definition 1 from the page I linked above), but when I click a link to the FDiv/CondFDiv file I get a 404 because it tries to send me to the doc page for the now nonexistent TestingLowerBound/CondFDiv.lean (try definition 2). I did not follow exactly what I did differently for one file or the other, and the issue might be present since many commits (I almost never click doc links). It is possible that I did not add anything to the blueprint referencing CondFDiv since the move? I am not sure.

[Patrick Massot]

I would say this is a doc-gen bug, not a blueprint bug. Look at https://remydegenne.github.io/testing-lower-bounds/docs/search.html?sitesearch=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib4_docs&q=ProbabilityTheory.condFDiv

[Patrick Massot]

@Henrik Böving

[Patrick Massot]

The doc-gen search turns up deadlinks.

[Henrik Böving]

Just so I don't do this for nothing @Rémy Degenne have you build the documentation for this standalone and verified it doesnt work as well?

[Henrik Böving]

Okay doing it mysefl was quicker than waiting for the answer.

If I build the docs locally and do the search everything works so it is either a bug in your specific setup or something else @Rémy Degenne @Patrick Massot

[Rémy Degenne]

Thanks for checking. I have never built any doc anywhere myself and I am not even sure of what you asked me to do precisely, so that was certainly faster :)

[Henrik Böving]

Basically what is described here: https://github.com/leanprover/doc-gen4/?tab=readme-ov-file#usage

[Rémy Degenne]

Thanks. I am building the doc (but it's taking forever on my bad laptop) and will check if it's also fine for me in local.

[Henrik Böving]

You will need to wait until the counter reaches 3825 on the left hand side.

[Rémy Degenne]

The build finally finished, and I confirm that my local doc is fine. No dead link.

[Patrick Massot]

What did you do that is not done by https://github.com/RemyDegenne/testing-lower-bounds/blob/master/.github/workflows/blueprint.yml?

[Rémy Degenne]

I only did lake -R -Kenv=dev build TestingLowerBounds:docs and then opened .lake/build/doc/, lanched a server and checked the same search as you did. Nothing more. The only difference I see with the "build documentation" step of that file is the -R flag in the build command. I don't know what that does of if it's relevant.

[Sam van G]

Following up on my message from earlier this week, and I think related to the above discussion: the CI for my blueprint is now working! @Floris van Doorn helped me with this yesterday.

[Sam van G]

The blueprint was already building locally immediately after installation, but the CI did not work. Even after adding -R to the same line in my blueprint.yml, the CI still failed, but with a different error, namely the dependency on doc-gen4 not being installed. We then also added this line.
I already forgot why we made these changes and why it works now, but perhaps Floris can explain that if needed.

[Yaël Dillies]

Rémy Degenne said:

I only did lake -R -Kenv=dev build TestingLowerBounds:docs and then opened .lake/build/doc/, lanched a server and checked the same search as you did. Nothing more. The only difference I see with the "build documentation" step of that file is the -R flag in the build command. I don't know what that does of if it's relevant.

Using the -K flag without the -R flag is always incorrect. So the fact you previously didn't include -R seems relevant

[Patrick Massot]

Interesting. I certainly did not invent that line, so this error must be elsewhere. @Rémy Degenne could you try putting that -R everywhere you see a -K in your ci file?

[Rémy Degenne]

added. Let's wait for CI.

[Rémy Degenne]

nope, that did not fix the issue.

[Patrick Massot]

I really hate CI. I already spent countless hours shooting in the dark to try to get things to work. I really don’t know what to do.

[Rémy Degenne]

removing the two following lines from the previous "Cache mathlib docs" step fixed it, but caused a full 12min mathlib doc build

.lake/build/doc/declarations
!.lake/build/doc/declarations/declaration-data-TestingLowerBounds*

[Rémy Degenne]

I don't know what I am doing and I deleted the two last lines because they were after the one mentioning mathlib... I may have deleted a line too much. My guess was that something was cached that should have been built again

[Rémy Degenne]

and now I don't have a failing doc to test on :shrug:

[Henrik Böving]

The file that was most likely cached was declarations/declaration-data.bmp which is an accumulation of all other files in declarations/

[Patrick Massot]

A caching issue definitely makes sense here.

[Pietro Monticone]

I've opened a PR fixing the issues mentioned above and a few typos in console.printed messages.

[Rémy Degenne]

You write that your PR fixes the issues mentioned above: which issues more precisely? Adding the -R flag everywhere as you do in the PR did not fix the doc issue I was having. I still don't really know how to fix that issue. I repaired my doc by not using the cache, but that's not a fix.

[Sam van G]

Rémy Degenne said:

removing the two following lines from the previous "Cache mathlib docs" step fixed it, but caused a full 12min mathlib doc build

Every time we execute the blueprint CI it now takes around 12 minutes (see here )... I thought that was normal but I understand from this remark it is not?
(Sorry for these probably obvious questions, I'm not at all familiar with leanblueprint, neither with the intricacies of CI on Github.)

[Rémy Degenne]

See the "Build documentation" of the run here to compare with yours: https://github.com/RemyDegenne/testing-lower-bounds/actions/runs/8491768981/job/23264057251
I my case, nothing in Mathlib is listed there, and the doc build step is under two minutes.

[Rémy Degenne]

But your CI run looks significantly different that mine (with steps "update docgen4" and "update checkdecls" that mine does not have)... so it might be hard to find the significant difference.
My blueprint was created from an earlier leanblueprint version. I will update it to match what the latest leanblueprint before commenting more on that.

[Rémy Degenne]

Some of your runs are short, like this one, which does not build the mathlib doc: https://github.com/samvang/StoneDualityInLean/actions/runs/8478789948/job/23231715503

[Rémy Degenne]

In your slow CI runs, the update docgen4 step contains a download of a new mathlib cache, while in your fast runs it only decompresses files (no download). Then in the slow runs the mathlib doc is built again, while in the fast runs it is not. Sorry that's incorrect. I now saw an example where there is a download and still no mathlib doc build, here: https://github.com/samvang/StoneDualityInLean/actions/runs/8471321425/job/23211010792

[Rémy Degenne]

An unrelated remark on that CI: the mathlib cache files are downloaded and decompressed at "update docgen4", then decompressed again at "update checkdecls" and again at "get cache" (and that last step seems completely useless).

[Yaël Dillies]

If you write a detailed explanation to what's going wrong, I can try fixing your CI at some point this afternoon

[Pietro Monticone]

Rémy Degenne said:

You write that your PR fixes the issues mentioned above: which issues more precisely? Adding the -R flag everywhere as you do in the PR did not fix the doc issue I was having. I still don't really know how to fix that issue. I repaired my doc by not using the cache, but that's not a fix.

Oh, I see... I was having docs issues (see https://github.com/pitmonticone/FLT3/actions) and they were apparently solved by adding the -R flag everywhere. I erroneously thought they were the same docs issues, sorry.

[Kevin Buzzard]

I tried to set up leanblueprint after an OS upgrade to Ubuntu 24.04 broke it, and now I can only get it working with a hack. If I try installing with pip I get

buzzard@brutus:~/lean-projects/FLT$ pip3 install -U leanblueprint
error: externally-managed-environment

× This environment is externally managed
╰─> To install Python packages system-wide, try apt install
    python3-xyz, where xyz is the package you are trying to
    install.

    If you wish to install a non-Debian-packaged Python package,
    create a virtual environment using python3 -m venv path/to/venv.
    Then use path/to/venv/bin/python and path/to/venv/bin/pip. Make
    sure you have python3-full installed.

    If you wish to install a non-Debian packaged Python application,
    it may be easiest to use pipx install xyz, which will manage a
    virtual environment for you. Make sure you have pipx installed.

    See /usr/share/doc/python3.12/README.venv for more information.

note: If you believe this is a mistake, please contact your Python installation or OS distribution provider. You can override this, at the risk of breaking your Python installation or OS, by passing --break-system-packages.
hint: See PEP 668 for the detailed specification.
buzzard@brutus:~/lean-projects/FLT$

I tried installing with pipx, which worked (I should say that I have no clue what I'm doing):

buzzard@brutus:~/lean-projects/FLT$ which leanblueprint
/home/buzzard/.local/bin/leanblueprint
buzzard@brutus:~/lean-projects/FLT$

and

buzzard@brutus:~/lean-projects/FLT$ file /home/buzzard/.local/bin/leanblueprint
/home/buzzard/.local/bin/leanblueprint: symbolic link to /home/buzzard/.local/pipx/venvs/leanblueprint/bin/leanblueprint
buzzard@brutus:~/lean-projects/FLT$

but now I have

buzzard@brutus:~/lean-projects/FLT$ which plastex
buzzard@brutus:~/lean-projects/FLT$ leanblueprint web
/bin/sh: 1: plastex: not found
Command 'plastex -c plastex.cfg web.tex' returned non-zero exit status 127.
buzzard@brutus:~/lean-projects/FLT$

I know which plastex leanblueprint wants though:

buzzard@brutus:~/lean-projects/FLT$ ls /home/buzzard/.local/pipx/venvs/leanblueprint/bin
activate      activate.fish  leanblueprint  plastex     python   python3.12  unidecode
activate.csh  Activate.ps1   markdown-it    pygmentize  python3  rich-click
buzzard@brutus:~/lean-projects/FLT$

so I can just add this directory to my $PATH (the hack) and now everything seems to work, but I'm pretty sure this is not what I'm supposed to be doing. I'm pretty sure that on Ubuntu 22 I just had the package installed globally (this is a single-user machine) and plastex installed via apt. I just want a pain-free installation. Any recommendations?

PS after the hack, it works fine but I get a warning:

warning: ././.lake/packages/checkdecls/././Main.lean:17:17: `Array.concatMap` has been deprecated, use `Array.flatMap` instead

which I'm ignoring.

[Ruben Van de Velde]

Ugh, python packaging

[Kevin Buzzard]

My instinct is that I don't want a virtual environment but is this somehow inevitable? Is this like me saying "forget elan, I just want one version of Lean installed and I want all my lean projects to work?"

[Ruben Van de Velde]

Yes, pretty much exactly (except maybe with "mathlib" more than "lean")

[Ruben Van de Velde]

Did pipx say what version of leanblueprint it installed?

[Kevin Buzzard]

buzzard@brutus:~/lean-projects/FLT$ pipx uninstall leanblueprint
uninstalled leanblueprint! ✨ 🌟 ✨
buzzard@brutus:~/lean-projects/FLT$ pipx install leanblueprint
⚠️  Note: leanblueprint was already on your PATH at
    /home/buzzard/.local/pipx/venvs/leanblueprint/bin/leanblueprint
  installed package leanblueprint 0.0.16, installed using Python 3.12.3
  These apps are now globally available
    - leanblueprint
done! ✨ 🌟 ✨
buzzard@brutus:~/lean-projects/FLT$

[Kevin Buzzard]

(oops, note the hack :-) )

[Kevin Buzzard]

I removed the dodgy dir from my PATH, uninstalled and reinstalled and I still get 0.0.16, without the note.

[Ruben Van de Velde]

Fascinating. https://github.com/PatrickMassot/leanblueprint is only up to 0.0.15

[Henrik Böving]

No it isn't https://github.com/PatrickMassot/leanblueprint/releases/tag/v0.0.16

[Henrik Böving]

The version number in that tar ball is right so it seems this was just never pushed to the master branch

[Ruben Van de Velde]

"This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository."

[Kevin Buzzard]

Huh, I just noticed that my LaTeX install is also broken: if I compile my blueprint in VS Code using LaTeX workshop I get

...
Chapter 10.
[47] [48] [49] [50] [51] [52] [53]) (./chapter/biblio.tex (../print/print.bbl [54] [55]))) [56] (../print/print.aux) )
(see the transcript file for additional information)
Output written on ../print/print.pdf (57 pages).
SyncTeX written on ../print//print.synctex.gz.
Transcript written on ../print//print.log.
Latexmk: No log file was found, neither the expected one, 'print.log', nor one in '.'.
Latexmk: fls file doesn't appear to have been made.
Latexmk: Couldn't read log file 'print.log':
  No such file or directory
----------------------
This message may duplicate earlier message.
Latexmk: Failure in processing file '/media/buzzard/ExternalSSD1TB/lean-projects/FLT/blueprint/src/print':
   *LaTeX didn't generate the expected log file 'print.log'

No idea if this is related. NB the logfile is there:

buzzard@brutus:~/lean-projects/FLT/blueprint/print$ ls -l print.log
-rw-rw-r-- 1 buzzard buzzard 48087 Dec  1 21:19 print.log

(the date and time is now)

[Julian Berman]

This is the same issue you had a few weeks ago

[Julian Berman]

There are two things to check, neither of which I've done but I can

[Julian Berman]

One is probably that leanblueprint probably should not rely on having plastex on PATH

[Julian Berman]

It depends on it presumably, so it should simply invoke sys.executable. that's clearly not something you do as a user but I'll look later

[Julian Berman]

The second is to look how to get pipx to link two binaries from one install

[Julian Berman]

I used to know how to do this but uv is way better than pipx so I've now forgotten

[Julian Berman]

But you can either look that up in the pipx docs or tell me you can't find it and I'll go find it when I'm at a computer

[Julian Berman]

That latex error looks unrelated but I have no idea what it means yet

[Ruben Van de Velde]

Can you try pipx install --include-deps leanblueprint?

[Kevin Buzzard]

buzzard@brutus:~/lean-projects/FLT$ pipx install --include-deps leanblueprint
⚠️  File exists at /home/buzzard/.local/bin/unidecode and points to
    /home/buzzard/.local/bin/unidecode, not
    /home/buzzard/.local/pipx/venvs/leanblueprint/bin/unidecode. Not
    modifying.
⚠️  File exists at /home/buzzard/.local/bin/markdown-it and points to
    /home/buzzard/.local/bin/markdown-it, not
    /home/buzzard/.local/pipx/venvs/leanblueprint/bin/markdown-it. Not
    modifying.
⚠️  File exists at /home/buzzard/.local/bin/pygmentize and points to
    /home/buzzard/.local/bin/pygmentize, not
    /home/buzzard/.local/pipx/venvs/leanblueprint/bin/pygmentize. Not
    modifying.
⚠️  File exists at /home/buzzard/.local/bin/rich-click and points to
    /home/buzzard/.local/bin/rich-click, not
    /home/buzzard/.local/pipx/venvs/leanblueprint/bin/rich-click. Not
    modifying.
  installed package leanblueprint 0.0.16, installed using Python 3.12.3
  These apps are now globally available
    - leanblueprint
    - plastex
    - markdown-it (symlink missing or pointing to unexpected location)
    - pygmentize (symlink missing or pointing to unexpected location)
    - rich-click (symlink missing or pointing to unexpected location)
    - unidecode (symlink missing or pointing to unexpected location)
done! ✨ 🌟 ✨
buzzard@brutus:~/lean-projects/FLT$

I have no memory of how I installed all that other stuff. My guess is that when I installed leanblueprint globally (when I was allowed to do that) all that other stuff got installed globally too.

[Kevin Buzzard]

Looks like it works but it might break randomly later on I guess?

[Kevin Buzzard]

buzzard@brutus:~/lean-projects/FLT$ ls -l /home/buzzard/.local/bin/unidecode /home/buzzard/.local/bin/markdown-it /home/buzzard/.local/bin/pygmentize /home/buzzard/.local/bin/rich-click
-rwxrwxr-x 1 buzzard buzzard 220 Apr  4  2024 /home/buzzard/.local/bin/markdown-it
-rwxrwxr-x 1 buzzard buzzard 215 Apr  4  2024 /home/buzzard/.local/bin/pygmentize
-rwxrwxr-x 1 buzzard buzzard 213 Apr  4  2024 /home/buzzard/.local/bin/rich-click
-rwxrwxr-x 1 buzzard buzzard 213 Nov 26  2023 /home/buzzard/.local/bin/unidecode
buzzard@brutus:~/lean-projects/FLT$

I suspect I installed leanblueprint globally in April but apparently unidecode was something I needed in 2023.

[Ruben Van de Velde]

In your position, I might delete the old ones and let pipx reinstall them

[Kevin Buzzard]

I now get some more exciting warnings:

buzzard@brutus:~/.local/bin$ mv markdown-it old_markdown-it
buzzard@brutus:~/.local/bin$ mv pygmentize old_pygmentize
buzzard@brutus:~/.local/bin$ mv rich-click old_rich-click
buzzard@brutus:~/.local/bin$ mv unidecode old_unidecode
buzzard@brutus:~/.local/bin$ cd
buzzard@brutus:~$ pipx uninstall leanblueprint
uninstalled leanblueprint! ✨ 🌟 ✨
buzzard@brutus:~$ pipx install --include-deps leanblueprint
⚠️  Note: markdown-it was already on your PATH at /usr/bin/markdown-it
⚠️  Note: pygmentize was already on your PATH at /usr/bin/pygmentize
  installed package leanblueprint 0.0.16, installed using Python 3.12.3
  These apps are now globally available
    - leanblueprint
    - markdown-it
    - plastex
    - pygmentize
    - rich-click
    - unidecode
done! ✨ 🌟 ✨
buzzard@brutus:~$

[Kevin Buzzard]

So apparently already my system was using a "random" pygmentize depending on which of /usr/bin and ~/.local/bin was first in my $PATH

[Kevin Buzzard]

My instinct is that leanblueprint is now likely to be working correctly, and there's a small chance that I broke something else, but given that I only use this machine to prove FLT and occasionally read emails / write references, I'll definitely take that. Thanks!

[Kevin Buzzard]

Having now dared to look at my PATH I see /home/buzzard/.local/bin is on it three times :-)

[Notification Bot]

6 messages were moved from this topic to #FLT > VS Code LaTeX Workshop issue by Kevin Buzzard.

[Patrick Massot]

Sorry for the forgotten push to master that confused people. I just fixed that.

[Patrick Massot]

However the issue really seems to be that Kevin has installed half of the tool globally and half locally.

[Kevin Buzzard]

Because my OS will no longer let me install it globally for some (perhaps good) reason

[Patrick Massot]

It’s true that the leanblueprint client could work a little harder to avoid calling plastex using the system. You can create an issue about that. But I’m pretty sure that having a saner python setups would bring other benefits. And I know it’s not so easy, especially when you have no interest in this and keep following random advice and forgetting what you did last time (which is perfectly legitimate). I wish this could be easier.

[Kevin Buzzard]

Yes you've very accurately summarised my situation.

[Kevin Buzzard]

Given that it's unlikely that I'll be doing any installing or uninstalling of anything on this computer other than dutifully bumping my OS to the next Ubuntu stable in a couple of years, I think we're safe for now! Thanks to everyone who helped!

[Jon Eugster]

So I just managed to get leanblueprint running on macOS after a few errors, the sequence of commands was something like this:

brew install graphviz
brew install python@3.12.                        # cannot be 3.13+
python3.12 -m venv .python
source .python/bin/activate
export C_INCLUDE_PATH=/opt/homebrew/include      # maybe not necessary
export LIBRARY_PATH=/opt/homebrew/lib            # maybe not necessary
pip install pygraphviz
pip install leanblueprint
leanblueprint all

One important point is that pygraphviz seems not run on python 3.13 (see here).

Just for reference, I guess