lean lexer (pygments)

Stream: general

[Joseph Corneli]

FYI I found and reported the following bug in the LeanLexer: #1459: LeanLexer does not have a "^" operator. The fix is simple, but my BitBucket account is locked so I can't submit the fix myself! (... Though I guess I could register another account there easily enough ...) Maybe it's worth setting up a stress-test for the Lexer to make sure that it has all the other required syntax?

[Gabriel Ebner]

BTW, we're using a pygments fork for the reference manual, etc.: https://bitbucket.org/gebner/pygments-main/src/default/

[Gabriel Ebner]

The upstream pygments project is unfortunately not very active. The lean highlighting there is still from Lean 2.

[Patrick Massot]

And we still need to bring this fork to use in Zulip...

[Joseph Corneli]

The upstream pygments project is unfortunately not very active. The lean highlighting there is still from Lean 2.

Thanks for the tip! I installed the fork, and got a replacement version of sphinx set up with the correct requirement 'Pygments==2.1a0.dev20180725', in setup.py. No problems with this version of the LeanLexer.

[William DeMeo]

Is anyone else having trouble with Pygments? I'm getting the error WARNING: Could not lex literal_block as "lean". Highlighting skipped. with valid lean code when I try to make html with sphinx. What version of Pygments is working well with Lean and how do I install it and make sure that's the version that is being used when I do make html. Any/all suggestions would be much appreciated!

[William DeMeo]

@Joseph Corneli Can you share with me the "simple fix" you found for getting lexer to lex specific symbols, e.g., ^? Right now I'm getting an error with valid Lean code, I think because of the presence of certain symbols such as these: ⋂₀, Π, ↑, ∘.

[Reid Barton]

Are you using @Gabriel Ebner's fork of pygments? https://bitbucket.org/gebner/pygments-main/src/default/

[William DeMeo]

@Reid Barton thanks for the suggestion. It's hard for me to know version I'm using. I did clone Gabriel Ebner's fork of pygments and I installed it with the command pip3 install Pygments. Nothing changed. I then tried @Joseph Corneli 's suggestion from last July, adding version = '2.1a0.dev20180725', to the setup.py file in the pygments-main directory and (re)installed pygments with the command sudo python3 setup.py install It seems to have installed successfully. (I get the response Installed /usr/local/lib/python3.6/dist-packages/Pygments-2.1a0.dev20180725dev_20190512-py3.6.egg among lots of other output.) Nothing changed. The lexer still fails to lex correct Lean code involving the symbols I mentioned above.

[William DeMeo]

Next I tried to replicate the setup of the Logic and Proof book as closely as possible. This sets up a fresh install of needed dependencies in a local directory called .venv, when one invokes make install-deps(in particular, this make directive installs pygments with pip3 install https://bitbucket.org/gebner/pygments-main/get/default.tar.gz#egg=Pygments. However, after make install-deps completes successfully, I invoke make html and I get the following weird output:
``Running Sphinx v2.0.1

Extension error:
Could not import extension sphinx.builders.epub3 (exception: No module named 'sphinxcontrib.serializinghtml')
Makefile:35: recipe for target 'html' failed
make: *** [html] Error 2``

...which is strange because I have compiled the Logic and Proof book before and it worked fine. Well, I'll keep hacking away at this for a while, but may have to let it go unresolved for now.

[William DeMeo]

Out of curiosity, I tried the following experiment: I inserted the seemingly unlexable bit of Lean code (code that includes symbols like ↑ and ∘) into a code-block of my fork of the Logic and Proof book and tried make html, and low and behold, the lexer could handle it... so clearly there's something wrong with the setup of my other project. When I resolve it, if there's any useful information that comes out of this, I'll post again. Thanks again for your help!