Current state of dependency management

Stream: lean4

[Patrick Massot]

I haven't followed the discussions about the very complicated issue of having a Lean library requiring more than Mathlib (and its dependency). What is the state of the art? Concretely, does anyone knows how to start a library depending on Mathlib and Partax? Right now Partax has lean toolchain 4.3.0 and Mathlib has lean toolchain 4.4.0-rc1. I would like to tell lake: use Lean 4.3.0 in my project with the latest Mathlib compatible with 4.3.0 and the latest Partax. I tried various things but without any luck. Note that using any version of Mathlib compatible with 4.3.0 would already be a good start. @Mac Malone

[Patrick Massot]

Note this should be a trivial case since Mathlib and Partax have no common dependency.

[Mac Malone]

Also, fortunately, Mathlib has release tags that mirror the Lean 4 version, so you should just be able to require mathlb from <url> @ "v4.3.0".

[Patrick Massot]

This is the very first thing I tried.

[Patrick Massot]

I tried editing the project lean-toolchain and lakefile to put 4.3.0 everywhere.

[Mac Malone]

Oh! What happened?

[Patrick Massot]

But somehow std still gets messed up.

[Mac Malone]

That's weird.

[Patrick Massot]

I'll try again from the beginning.

[Patrick Massot]

There are so many steps and each step can mess up the work of the previous step so the order is crucial.

[Patrick Massot]

Weirdly enough, it looks like it worked this time.

[Mac Malone]

As an aside, if you plan to use Partax for compiling large parser categories (e.g., ones including term), I want to warn you that it will take some time (a few minutes), as I have not had time to work on optimizing the parser compiler.

[Patrick Massot]

I understand this needs to be avoided. I'd like to define my own syntax category and compile that.

[Mac Malone]

Great! In that case, it should hopefully work well!

[Patrick Massot]

Is there any documentation besides the README?

[Patrick Massot]

import Partax

declare_syntax_cat test

syntax "foo" : test

syntax "bar" : test

open scoped Partax

compile_parser Lean.Parser.Category.test => testParser

fails :sad:

[Patrick Massot]

Mac Malone said:

As an aside, if you plan to use Partax for compiling large parser categories (e.g., ones including term), I want to warn you that it will take some time (a few minutes), as I have not had time to work on optimizing the parser compiler.

Actually maybe I misunderstood that comment. The syntax I want to be able to parse obviously contain terms. Does that mean I can't use Partax? And those few minutes, are they only when building the parser or also whenever using the parser?

[Mac Malone]

Patrick Massot said:

Is there any documentation besides the README?

@Patrick Massot Sadly, not much. However, this case is covered by the README. To compile parser categories, one uses compile_parser_category instead of compile_parser.

[Patrick Massot]

I tried

import Partax

declare_syntax_cat test

syntax "foo" : test

syntax "bar" : test

open scoped Partax

compile_parser_category Lean.Parser.Category.test

but it also fails

[Patrick Massot]

It says: parser 'Lean.Parser.Category.test' is missing a 'keywords : NameSet' definition

[Mac Malone]

Patrick Massot said:

The syntax I want to be able to parse obviously contain terms. Does that mean I can't use Partax? And those few minutes, are they only when building the parser or also whenever using the parser?

You can use Partax, it just means compiling the term category will take a few minutes. The compiled parser will be fast, just the building is slow. You can cache the result by sticking the compilation of term in a separate module. (Partax does this with Partax.Test.LCompile.)

[Mac Malone]

Patrick Massot said:

I tried
[...]
but it also fails

Sorry, I should have been more specific. To compile a category, use compile_parser_category <category-name>. For instance, compile_parser_category test in your example.

[Mac Malone]

@Patrick Massot Also, I did verify that Partax builds on v4.4.0-rc1, so you should also be able to use it with the latest Mathlib.

[Patrick Massot]

Ok, compile_parser_category test works (I mean it does not bring any error message), thanks.

[Patrick Massot]

Is the next step to put import Partax.Test.LCompile to get terms?

[Mac Malone]

Here is a complete version of your example:

import Partax

declare_syntax_cat test

syntax "foo" : test

syntax "bar" : test

open scoped Partax

compile_parser_category test

#eval test.run' "foo" -- Except String (TSyntax `test)

[Mac Malone]

Patrick Massot said:

Is the next step to put import Partax.Test.LCompile to get terms?

That will only get you the core terms/commands. If you wan tthe Mathlib ones, you will need to do the same as LCompile but after an import Mathlib (and an open scoped of any relevant namespace defining more scoped terms/commands).

[Patrick Massot]

Did you actually ever tried that? How long did it take?

[Mac Malone]

@Patrick Massot No, I have not tried compiling Mathlib parsers. I do not imagine it will take orders of magnitude longer (e.g., it will likely take several minutes rather than a few). The definitions Partax creates are not mutual, so the time should scale approximately linearly (especially as the primary time sink is elaboration time).

[Mac Malone]

I can go give it a shot an report back if you want.

[Patrick Massot]

I can already tell you 15 minutes are not enough on my computer.

[Mac Malone]

wow

[Patrick Massot]

I'll have lunch now and see whether a lunch time is enough.

[Mac Malone]

I wonder how many parsers mathlib defines...

[Mario Carneiro]

not that many

[Mac Malone]

@Mario Carneiro Note this includes syntax/notation declarations.

[Mario Carneiro]

at least not term parsers, but I suppose the term grammar is mutual with tactic and mathlib defines a lot of those

[Mac Malone]

Ah, yes, term includes tactic.

[Mario Carneiro]

is it possible to not go through the elaborator here?

[Mac Malone]

@Mario Carneiro Yes, that would be the optimization I should spend time on.

[Mac Malone]

I just haven't had the time (no pun intended).

[Mario Carneiro]

I'm sure you have better things to do with your time :wink:

[Patrick Massot]

35 minutes is not enough, so I'll declare this approach unsuitable for anything involving Mathlib.

[Mario Carneiro]

what is your motivation for using Partax in the first place?

[Mac Malone]

:sad: That's probably fair.

[Patrick Massot]

Mario, the context is Lean verbose, my controlled natural language for teaching library. I ported the help tactic which suggest tactics. Currently this help tactic outputs strings but there is nothing checking that those strings are valid tactics. If I modify the syntax of a tactic and forget to update the help tactic then users get misleading advice. So I tried to build syntax in the help tactic. But this is super painful. So my next idea was to keep producing strings but try to parse them before suggesting them. This is where Partax sounded useful. But I guess I should simply try runParserCategory.

[Mario Carneiro]

yes you should

[Mario Carneiro]

although, it's also strange that your syntax wouldn't parse

[Mac Malone]

Yes, in the context of a tactic, runParserCategory is probably much better anyway (as there is already a proper Lean environment).

[Mario Carneiro]

in what way is it painful to build syntax?

[Patrick Massot]

Mario Carneiro said:

although, it's also strange that your syntax wouldn't parse

I don't understand what you mean.

[Mario Carneiro]

if you pretty print syntax it always parses (outside a few rare edge cases)

[Mario Carneiro]

so it is definitely recommended to construct syntax and pretty print it instead of building a string

[Mario Carneiro]

this is how tryThis works

[Patrick Massot]

The problem is not to pretty-print syntax, it is to build syntax. Mostly because the quotation syntax is so brittle and needs random type ascriptions all over the place.

[Mario Carneiro]

hm, my recommendation is still to use syntax quotations but maybe there is a specific issue that comes up?

[Patrick Massot]

It always end up working, sometimes after getting help, but it's a huge work compared to building a string.

[Patrick Massot]

So building a string and parsing it seems a lot easier.

[Mario Carneiro]

well you are talking about brittle solutions, producing a string is very brittle

[Patrick Massot]

I know that string production alone is super brittle, this is why I'm trying various ways to produce syntax.

[Mario Carneiro]

well reparsing won't help, it will just change the way that the tactic breaks

[Patrick Massot]

The goal is to catch breaking before users see it.

[Mario Carneiro]

it really sounds to me like syntax quotations are the right way to go, even if they are fiddly

[Patrick Massot]

The library has tests, but currently they don't try the suggestions.

[Mario Carneiro]

because only you have to deal with that, not users

[Patrick Massot]

Ok, I'll try again quotations. Let's pick an example. Given n : Name, a string such as " ≥ " and e : Expr, how would you produce syntax for n ≥ e?

[Mario Carneiro]

there is no "such as" for syntax in that position, you would have to pattern match it and handle them separately

[Patrick Massot]

I mean without first producing a string and then parsing it...

[Patrick Massot]

Ok, let's say the relation is fixed.

[Mario Carneiro]

let n := mkIdent n
match s with
| "≥" => `($n:ident ≥ $e)
| ...

[Patrick Massot]

Does that really work without delaborating e first?

[Mario Carneiro]

oh I missed that e is not syntax

[Mario Carneiro]

no you need to call delab on it first

[Patrick Massot]

Ok, so this is indeed a lot of work. Doable but a lot of work.

[Siddhartha Gadgil]

A related question: is there a convenient method similar to runParserCategory but which parses a maximal initial piece matching the syntax? Currently I solve this by copy-pasting and modifying from runParserCategory.

[Mario Carneiro]

no