Adjust _RocqProject parsing to rocq makefile changes - #880
Conversation
Is this based on experimenting with |
|
This seems to work fine with the _RocqProject I was trying to use earlier. :) |
Reading the code. It used to just dump whatever you added into Makefile, and that's how I wrote the original code. Then that changed, and my -arg code broke. So I rewrote the -arg code to track the new rocq makefile closely. |
|
Thanks @cpitclaudel ! LGTM. The errors in the CI seem unrelated (problem with the generation of to files with same date stamp). |
|
Thanks! I'll have a quick look at fixing the tests and then I'll merge |
These tests were broken by fine grained timestamps on CI.
This is an attempt to follow `lib/coqProject_file.ml` instead of doing our own parsing: - `#` starts a comment line; - Single quotes toggle quoting and get stripped; - `\` isn't an escape character, so `-arg "-w \"a b\""` (which we used to accept) now needs to be written `-arg "-w 'a b'"`. Fixes #113, #392, #522, #589. Closes #879.
475d4e6 to
73d461f
Compare
|
@Matafou I fixed the par tests; can you have a look? I did my best at reconstructing what the tests meant ^^ |
|
FWIW I updated and clarified the docs for this on the Rocq side in rocq-prover/rocq#22322 and rocq-prover/rocq#22369, and also fixed the odd behavior Rocq had when there were unpaired |
|
nice, thanks. Pushed a new version |
3 participants
This is an attempt to follow
lib/coqProject_file.mlinstead of doing our own parsing:#starts a comment line;\isn't an escape character, so-arg "-w \"a b\""(which we used to accept) now needs to be written-arg "-w 'a b'".Fixes #113, #392, #522, #589. Closes #879.