Gabriel Hondet

My concern is rather that the syntax of identifiers is not really clear. It seems odd to me to allow `/` by itself but not in anything else. IMO nobody...

I think we can close this issue, we already have the documentation available.

Ah yes, we can do as indicated in https://ocamlverse.github.io/content/documentation_guidelines.html I guess

> @gabrielhdt How do you plan to introduce in LP the rules you want to use? If I remember well, dkmeta takes as argument some file f_in.dk and some set...

We may also be more general, and allow to evaluate any command once the input is parsed. This would allow for instance to declare a symbol `abst` and a rewrite...

A possible implementation of LpMeta may behave as specified by the following test file https://github.com/Deducteam/personoj/blob/48d580f39975292ae8ad5af9136f19b56a324b44/proofs/psnj_toolbox/test/qfo/qfo.t where the binary lpmeta is called `psnj qfo` (for historical reasons, it should be changed)....

Well for the moment it's rather only an API, so it allows to rewrite terms, and not file or signature. But rewriting files or signature should only depend on the...

Is this still relevant? Aren't we happy with the current behaviour being that function application has always the highest priority? Plus I think it would introduce some complexity regarding the...

This is kind of fixed by #1090 because the dune related install is abandoned.

If I understand correctly, this issue would be fixed by implementing `libnss_files` on top of musl, which may be a lot of work. While we wait for such an implementation,...