Open aleloi opened 1 year ago
Hmm, I haven't encountered that issue, though I do think I was able to run a search report on math-comp recently. I'll look into it deeper when I have time, thanks for reporting!
Hi @HazardousPeach and thanks for the answers! I would also like to evaluate on mathcomp. Do you remember roughly how you did the evaluation? I am using proverbot9001.py search-report
, maybe you were running it differently? I've seen that there is src/search_file_cluster.py
I have gotten help from the SerAPI zulip with this issue: the problem is that coq_serapy replaces proofs with Admitted
and expects the resulting proof script to be valid. On rare occasions this can change the type: consider the example from choice.v
above with
Section OtherEncodings.
Variables T T1 T2 : Type.
...
Lemma tag_of_pairK : cancel tag_of_pair pair_of_tag. Admitted.
End OtherEncodings.
Prenex Implicits tag_of_pairK.
This fails because the lemma was originally tag_of_pairK : (T1 T2: Type) -> cancel ...
. After changing the proof to Admitted, Coq doesn't know that the proof does not use the variable T: Type
, and the type changes to tag_of_pairK : (T T1 T2: Type) -> cancel ...
.
In the end the workers fail because coq_serapy raises coq_serapy.CoqExn and it is never handled. I've tried to catch it somewhere. My goal was to make proverbot skip all further jobs in that file. I have not managed to do that yet.
Ah okay, so the fix for this was actually already implemented it looks like, but only in the develop
branch. Yes, Proverbot9001 tries to admit proofs when it's not working on them to make processing faster. In some cases this doesn't work, so Proverbot9001 has a --careful
flag which runs the proofs all the way through instead of admitting them. On the version of the code you're already on, using that --careful flag should fix the problem. But it's annoying to have to figure out which files need that and do the correct flags, so the patch makes it so that if Proverbot gets an exception when running Vernac, it'll restart the file with --careful
. Now that patch is on the master
branch, so if you git pull everything should work.
Now my mathcomp evaluation crashes less often. But I don't think that @HazardousPeach 's latest fix fully fixes the issue. I think that the new code around these lines does not clean up the previous proof context correctly.
if not careful:
eprint(f"Hit a problem, possibly due to admitting proofs! Restarting file with --careful...",
guard=self.args.verbose >= 1)
self.reset_file_state()
self.exit_cur_file() # <- does not exit the right way?
self.enter_file(job_file) # <- runs self.coq.run_stmt(f"Module {module_name}.") without properly exiting the file context
self.run_into_job(job, restart_anomaly, True)
When I run on mathcomp, I get the error Modules and Module Types are not allowed inside sections.
. I did not investigate much further. Instead I added code to restart coq with the right switch at the place where you added code for restarting with --careful
. Now my evaluation runs without crashes.
I can make a PR with the coq-restarting change if you think it is the appropriate solution.
Sure that pull request sounds good! The restarting seems to work a bit better on develop, but involves changes across the submodule boundary which are hard to cherry-pick in, so if you have something self contained that would be better for now, until its time to merge larger changes into master.
I'm trying to create an evaluation report on the
coq-projects/math-comp
project. The result is an uncaught coq_serapy.CoqExn that brings down the worker pool. I have tried to create a minimal example:I'm running proverbot as
mathcomp_proj_split.json
is for running coq with the right switch:Proverbot runs without problems on the first few lemmas and even proves a few, but fails parsing a a command starting with
Prenex Implicits ...
. The output ends withI thought this is a SerAPI or issue and tried to create a minimal reproducing example. Here is one. Pasting the following to
~/.opam/coq-8.12/bin/sertop --implicit
produces the same error as Proverbot:I would like to her Proverbot developer's thoughts about this. Have you encountered something similar, and how did you solve it?