Jason Gross

> idea--the benefit of having _CoqProject files present is that you could then step through the package scripts in CoqIDE This is exactly what I meant by "navigation" (implicitly: within...

> IMHO, if a `_CoqProject` is available, we can install it, but given the ongoing changes in the way Coq projects are built (with Dune becoming an option), I wouldn't...

That all sounds good to me

> Is your `-R theories HoTT` a reference to a different installed package? No, I'm talking about https://github.com/HoTT/HoTT/blob/0cc34d174334830919eb46421ee0f4ef29a1418a/_CoqProject#L1 which is not suitable for being installed because while the source package...

I am not sure whether or not this is a bug in `coq_makefile`. I believe the current lexer is that a token is anything that matches `[^ "]+` or `"[^"]+"`...

Hm? There's exactly one level of unsafe shell argument interpolation: the one that's happens because we're using `make`. > `coq_makefile` claims that it can take "extra arguments" in a file,...

> No. But Coq makefile will diligently put things in the Makefile, to be executed by make later, and so things will be broken for our users, which is all...

> as there's a sane way for us to do the same thing in PG. How hard is it to implement coq_makefile's lexer? You split off tokens as space-separated not-containing...

Oh, I see, yes. Shell unescaping. But aren't you doing that already with `split-string-and-unquote`? Or does that not handle single-quoted strings?

Actually, easy kludge: can you just replace `'` with `\"` in the contents of `_CoqProject` before processing it? The only way this will break things, I think, is if the...