Zulip Chat Archive

Stream: general

Topic: lean lexer (pygments)


view this post on Zulip Joseph Corneli (Jul 25 2018 at 12:59):

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?

view this post on Zulip Gabriel Ebner (Jul 25 2018 at 13:08):

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

view this post on Zulip Gabriel Ebner (Jul 25 2018 at 13:08):

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

view this post on Zulip Patrick Massot (Jul 25 2018 at 14:34):

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

view this post on Zulip Joseph Corneli (Jul 25 2018 at 15:01):

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.

view this post on Zulip William DeMeo (May 12 2019 at 15:23):

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!

view this post on Zulip William DeMeo (May 12 2019 at 15:52):

@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: ⋂₀, Π, ↑, ∘.

view this post on Zulip Reid Barton (May 12 2019 at 15:55):

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

view this post on Zulip William DeMeo (May 13 2019 at 05:54):

@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.

view this post on Zulip William DeMeo (May 13 2019 at 06:00):

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.

view this post on Zulip William DeMeo (May 13 2019 at 06:15):

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!


Last updated: May 07 2021 at 00:30 UTC