--update-errors is missing some states
Now that I have been able to run --list-errors
, I can mention the actual bug (or not?) we have encountered in Why3. When running the following command on the files of the parser :
menhir parser.mly --update-errors handcrafted.messages
I get a file that is different from the one obtained by running
menhir --list-errors parser.mly
In particular, it seems to be missing about 30 cases. For example, the file generated by --compile-errors
does not have a branch for 79, which can be triggered by the input lemma err: (let x5 x6)
.
I am not sure we are using --update-errors
correctly, especially since --list-errors
takes two minutes while --update-errors
finishes instantly. Are we supposed to run --list-errors
regularly? If so, what is the proper way of recovering older custom error messages?