Add support for Lean 4 projects #5
Conversation
| @@ -47,7 +47,7 @@ name: thmenv | |||
| {% call modal('Lean declarations') %} | |||
| <ul class="uses"> | |||
| {% for lean, url in obj.userdata.lean_urls %} | |||
| <li><a href="{{ url }}">{{ lean }}</a></li> | |||
| <li><a href="{{ url }}" target="_blank" rel="noopener noreferrer">{{ lean }}</a></li> | |||
There was a problem hiding this comment.
I don't get why you want to impose the target="_blank" behavior. Why not assuming people know how they want to open links?
There was a problem hiding this comment.
Personally, I would always need the doc & source for a particular definition in a new tab, avoiding the disruption of navigating the dep graph or reading the blueprint. Choosing this every time is very inconvenient, especially on Mac without a mouse. I didn't think much on giving the choice to the readers, but provided an opinionated default.
While I'll need this default myself, I'm happy to revert these lines for the PR.
There was a problem hiding this comment.
Yes, I think this is too opinionated. And helping people to get away from Macs is always a good action. On a normal computer you simply middle-click on a link if you want to open it in a new tab. This is exactly the same effort as a left-click.
There was a problem hiding this comment.
In retrospect, indeed, it's too opinionated.
Instead, I'll add a CSS class leandecl to all Lean links, so one can easily add customized behaviors/styles to Lean links in JavaScript of their own blueprint repo. Is that more neutral and acceptable?
There was a problem hiding this comment.
Done in utensil#2 .
|
Thanks! |
|
|
||
| 1. Port your Lean 3 code to Lean 4, likely with the help of [mathport](https://github.com/leanprover-community/mathport) | ||
| 2. Set up [doc-gen4](https://github.com/leanprover/doc-gen4) for your project, publish it somewhere, e.g. https://your-docgen4-url-base/ | ||
| 3. The new plugin jumps to the documentation generated by `doc-gen4` for `\lean{YourLean4Theorem}` if you have specified `\dochome{https://your-docgen4-url-base/}` in your `web.tex` file. This is equivalent to the old plugin, which jumped to the source code of the theorem in your GitHub repository for `\lean{your_lean3_theorem}`. You need to carefully port all `\lean{your_lean3_theorem}` to `\lean{YourLean4Theorem}`, this could be just a search and replace with the CamelCase version of your theorem name, or it could have been renamed in your Lean 4 porting process. |
There was a problem hiding this comment.
I just realized that this line written in early commits is inaccurate, definitions would have case porting issues but not theorems according to Mathlib naming conventions, the example here is totally wrong (but not misleading because no one would be actually misled I guess). Will fix it in a follow-up PR (but I might wait for some other issues) or feel free to just fix it.
This PR adds support for Lean 4 projects in a minimal setting. Please see
Migration from Lean 3in README.md for how it works, and this Zulip thread for more context and discussion.It was initially made to be compatible with Lean 3 on the
lean4branch, and made "Lean 4 only" after some discussion on Zulip as it's unlikely for others to need to reference both Lean 4 projects and Lean 3 projects in one blueprint.This approach relies on the project to set up
doc-gen4, unlike the Lean 3 plugin relies onmathlibtoolsto generate the location of Lean declarations.