ASCII equivalents for angle brackets

Stream: new members

[Sam Estep]

As discussed a bit here, I'm starting to work on updating the code examples in the "Theorem Proving in Lean" book so that make leantest works in newer versions of Lean. I notice that the "ASCII equivalents" (| and |) to the angle bracket notation don't seem to work in Lean 3.18.4; have those been removed entirely, or is there a newer ASCII syntax that I can replace them with?

[Shing Tak Lam]

It was lean#265, and I don't think there's any ASCII aliases anymore.

[Jeremy Avigad]

@Sam Estep I was planning to try to update TPiL to 3.18.4 and the community online Lean within the next few days. Should I wait to do that? Are you planning to make a pull request?

[Sam Estep]

@Jeremy Avigad I was planning to, but if you’d rather do it instead then that also works! I apologize for failing to communicate better in that case

[Jeremy Avigad]

Either way is o.k. by me. I know both Lean and Sphinx pretty well, so I am hoping it won't be too difficult to do it all at once. But if you have made good progress and would like to finish it off, that is good to. (I see that I also missed a pull request on June 4 with a small correction, so I will also take care of that at the same time.)

Getting the system to use the new community online Lean requires small changes to Gabriel's Python code. I did that recently for MiL, so it shouldn't be hard to do it again for TPiL.

[Jeremy Avigad]

Oh, and while I am thinking about it, there is a place in the config file to update the version number, so we can say 3.18.

[Sam Estep]

@Jeremy Avigad Ok sounds good, thanks so much for working on this! Since you're much more skilled in both tools than I am, it would probably be much better and faster if you're the one who does it; the only progress I've made so far is setting up GitLab CI to automatically run the tests on each commit, and removing this one angle brackets example: https://gitlab.com/sestep/theorem_proving_in_lean/-/commit/b4cf0d31

[Sam Estep]

Regarding the version number, are you referring to these lines? https://github.com/leanprover/theorem_proving_in_lean/blob/2a995ba/conf.py#L52-L59 I didn't notice those at first, and ended up instead adding a leanpkg.toml file that specifies lean_version = "leanprover-community/lean:3.18.4", since that seems to actually change which version make leantest uses; not sure if that's worth doing on your end, but it might make it easier for people to reproduce the test results

[Jeremy Avigad]

Yes, those are the lines I had in mind. It just changes the version number in the PDF file. The right way to update the .toml file is to use leanproject up, which also fetches the new .olean files.

I just pushed the revisions -- I'll announce on a new thread.