search-report fails on the pinned math-comp version. coq_serapy.CoqExn: Expected prenex implicits for tag_of_pairK

[aleloi]

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

./src/proverbot9001.py search-report -j 1 --weightsfile=data/polyarg-weights.dat \
    --prelude=./coq-projects/ --search-depth=1 --verbose --verbose --verbose \ 
    --search-width=2 --splits-file=mathcomp_proj_split.json \
    -P ./math-comp/mathcomp/ssreflect/choice.v

mathcomp_proj_split.json is for running coq with the right switch:

[
    {
    "project_name": "math-comp",
    "test_files": [
        "mathcomp/ssreflect/choice.v"
    ],
    "switch": "coq-8.12"
}
]

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 with

Running statement: Prenex Implicits seq_of_optK tag_of_pairK pair_of_tagK opair_of_sumK.

Problem running statement: Prenex Implicits seq_of_optK tag_of_pairK pair_of_tagK opair_of_sumK.


Expected prenex implicits for tag_of_pairK
Failed getting to before: 
Lemma codeK : pcancel encode decode.

In file mathcomp/ssreflect/choice.v
Process Process-2:
Traceback (most recent call last):
  File "/home/alex/proverbot9001/coq_serapy/src/coq_serapy/__init__.py", line 404, in run_stmt
    self.feedbacks = self._get_feedbacks()
  File "/home/alex/proverbot9001/coq_serapy/src/coq_serapy/__init__.py", line 1330, in _get_feedbacks
    match(normalizeMessage(fin),
  File "/home/alex/proverbot9001/lib/python3.10/site-packages/pampy/pampy.py", line 299, in match
    return run(action, lambda_args)
  File "/home/alex/proverbot9001/lib/python3.10/site-packages/pampy/pampy.py", line 48, in run
    return action(*var)
  File "/home/alex/proverbot9001/coq_serapy/src/coq_serapy/__init__.py", line 1334, in <lambda>
    raise_(CoqExn(fin)),
  File "/home/alex/proverbot9001/coq_serapy/src/coq_serapy/__init__.py", line 123, in raise_
    raise ex
coq_serapy.CoqExn: [Symbol('Answer'), 132, [Symbol('CoqExn'), [[Symbol('loc'), [[[Symbol('fname'), Symbol('ToplevelInput')], [Symbol('line_nb'), 1], [Symbol('bol_pos'), 0], [Symbol('line_nb_last'), 1], [Symbol('bol_pos_last'), 0], [Symbol('bp'), 0], [Symbol('ep'), 69]]]], [Symbol('stm_ids'), [[42, 43]]], [Symbol('backtrace'), [Symbol('Backtrace'), []]], [Symbol('exn'), [Symbol('CErrors.UserError'), [Symbol('ssreflect'), 'Expected prenex implicits for tag_of_pairK']]], [Symbol('pp'), [Symbol('Pp_glue'), [[Symbol('Pp_glue'), []], [Symbol('Pp_string'), 'Expected prenex implicits for '], [Symbol('Pp_tag'), Symbol('constr.reference'), [Symbol('Pp_string'), Symbol('tag_of_pairK')]]]]], [Symbol('str'), 'Expected prenex implicits for tag_of_pairK']]]]

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/usr/lib/python3.10/multiprocessing/process.py", line 314, in _bootstrap
    self.run()
  File "/usr/lib/python3.10/multiprocessing/process.py", line 108, in run
    self._target(*self._args, **self._kwargs)
  File "/home/alex/proverbot9001/src/search_file.py", line 248, in search_file_worker
    solution = worker.run_job(next_job, restart=not args.hardfail)
  File "/home/alex/proverbot9001/src/search_worker.py", line 218, in run_job
    self.run_into_job(job, restart=restart)
  File "/home/alex/proverbot9001/src/search_worker.py", line 133, in run_into_job
    self.coq.run_into_next_proof(
  File "/home/alex/proverbot9001/coq_serapy/src/coq_serapy/__init__.py", line 493, in run_into_next_proof
    self.run_stmt(command, timeout=60)
  File "/home/alex/proverbot9001/coq_serapy/src/coq_serapy/__init__.py", line 440, in run_stmt
    self._handle_exception(e, stmt)
  File "/home/alex/proverbot9001/coq_serapy/src/coq_serapy/__init__.py", line 1001, in _handle_exception
    raise CoqExn(coqexn_msg)
coq_serapy.CoqExn: Expected prenex implicits for tag_of_pairK

I 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:

(Add () "Module choice.")
(Add () "From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.")
(Add () "Set Implicit Arguments.")
(Add () "Unset Strict Implicit.")
(Add () "Unset Printing Implicit Defensive.")


(Add () "Section OtherEncodings.")
  (Add () "Variables T T1 T2 : Type.")

  (Add () "Definition tag_of_pair (p : T1 * T2) := @Tagged T1 p.1 (fun _ => T2) p.2.")
  (Add () "Definition pair_of_tag (u : {i : T1 & T2}) := (tag u, tagged u).")
  (Add () "Lemma tag_of_pairK : cancel tag_of_pair pair_of_tag. ")
  (Add () "Admitted.")
(Add () "End OtherEncodings.")

(Add () "Prenex Implicits tag_of_pairK.")


(Exec 1)
(Exec 2)
(Exec 3)
(Exec 4)
(Exec 5)
(Exec 6)
(Exec 7)
(Exec 8)
(Exec 9)
(Exec 10)
(Exec 11)
(Exec 12)
(Exec 13)
(Exec 14)

I would like to her Proverbot developer's thoughts about this. Have you encountered something similar, and how did you solve it?

[HazardousPeach]

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!

[aleloi]

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.

[HazardousPeach]

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.

[aleloi]

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.

[HazardousPeach]

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.