[sercomp] add goals mode to print some proof goal info

[palmskog]

I'm trying to set up code for serialization via sercomp of some proof goal information, but am running into issues.

Consider the following example (pi.v):

From mathcomp Require Import all_ssreflect.
Lemma filter_pi_of n m : n < m -> filter \pi(n) (index_iota 0 m) = primes n.
move=> lt_n_m; have ltnT := ltn_trans; apply: (eq_sorted_irr ltnT ltnn).
- by rewrite sorted_filter // iota_ltn_sorted.
- exact: sorted_primes.
move=> p; rewrite mem_filter mem_index_iota /= mem_primes; case: and3P => //.
by case=> _ n_gt0 dv_p_n; apply: leq_ltn_trans lt_n_m; apply: dvdn_leq.
Qed.

Here, the second sentence results in one proof goal, while the third sentence results in three goals. So I would have expected that sercomp --mode=goals pi.v would print something like:

0
1
3
...

But instead I get:

0
1
0
...

Is there anything obvious I'm doing wrong?

[ejgallego]

the second sentence results in one proof goal

I think you are "counting" the sentences wrong. IIRC bullets are considered as sentences on their own, thus you will have:

0
1
0
3
0

You can use the other records of the goals field to get info about the goal stack I think.

[palmskog]

I changed the printing format to "X Y" where X is the number of goals and Y is the size of the stack, and "- -" if there is no goal and stack info. Here is the full output I get:

- -
1 0
- -
- -
- -
- -
- -
- -
- -
- -

So there seems to be something wrong with Stm calls, e.g., to Stm.observe. Any ideas?

[ejgallego]

I changed the printing format to "X Y" where X is the number of goals and Y is the size of the stack, and "- -" if there is no goal and stack info. Here is the full output I get:

That's bizarre, certainly I don't get that; but I ran it in 8.9; need to prepare a math-comp setup for 8.10.

[palmskog]

Here is another example without ssreflect/mathcomp and no bullets or other decoration.

Require Import Arith.
Definition update {A} (st : nat -> A) (h : nat) (v : A) := fun (n : nat) => if Nat.eq_dec n h then v else st n.
Lemma update_nop : forall A (st : nat -> A) y v, st y = v -> update st y v y = st y.
intros; unfold update.
case Nat.eq_dec; subst.
auto.
auto.
Qed.

The expected output is something like:

- -
- -
1 0
1 0
2 0
1 1
1 0
- -

But instead I get:

- -
- -
1 0
- -
- -
- -
- -
- -

However, sertop seems to work as expected with these examples (when using Add and Query Goals, etc.).

[ejgallego]

As discussed today, the problem here is the

  let ndoc = { Stm.doc_type = Stm.VoDoc in_file

in sercomp.ml, in particular VoDoc does disable immediate caching of proof states so goals won't be available later on when the query happens.

[ejgallego]

@palmskog , should this go into the 8.10 release? I think we can test the goals mode and use the Vio type.

[palmskog]

@ejgallego I want to include this into the 0.7.0 release, but I feel simply counting goals in a state is very limited and will not solve our use case. A better idea may be to actually print the goal structure in some form - I will experiment with this for a day or so and then we can make the final decision.

[ejgallego]

I will experiment with this for a day or so and then we can make the final decision.

Sounds good, you already have quite a lot of machinery in serapi_goal, which is used in the query goal, indeed this goal mode seems a bit limited, maybe you could directly use the main protocol?

I think 0.7.0 will still take quite a few days so no rush, also we can do a 0.7.1 very quickly if you need more time.

[ejgallego]

@palmskog any updates on this?

Would postponing for 0.7.1 be a problem for you folks?

[palmskog]

@ejgallego I'm stuck on something else right now, so postponing to 0.7.1 is fine.

[ejgallego]

@ejgallego I'm stuck on something else right now, so postponing to 0.7.1 is fine.

Ok, thanks! I think I will release 0.7.0 tomorrow and just postpone the package manager work and this to 0.7.1 ; IMHO having a new version in OPAM is overdue.

[palmskog]

Still seemingly can't get the desired output for the example file (pi.v) above, even with VioDoc. Any hints @ejgallego?

[ejgallego]

Thanks for the update @palmskog , I'll have a look.

[ejgallego]

VioDoc is indeed not the right thing to use, I've pushed a tweak + change entry.

IMHO this is ready to merge, maybe we should squash the commits tho.

[ejgallego]

Also, I did make the document creation conditional on the mode, that should fix the error suite bug:

Error: File "mbid.v", line 52, characters 0-17:
       Anomaly
       "True Future.t were created for opaque constants even if -async-proofs is off"
       Please report at http://coq.inria.fr/bugs/.
Done: 1832/1863 (jobs: 2)

That's a funny one tho! I wonder if Coq master still suffers from that bug.

[palmskog]

This looks great, many thanks for looking into the problem. However, the output format is currently very simplistic, I'm going to dig in a bit a day or two and see if I can figure out something more general. The goal is to be able to deduce proof structure in some form, which "number of open goals" seems inadequate for.

[ejgallego]

OK, thanks for the update @palmskog ; ping me if you want further review or just merge if not.

I think I'll have time next week to implement a few items from the 0.7.1 milestone; then I guess we can release 0.7.1 and focus on 0.11.0 [for Coq 8.11]

[ejgallego]

Removing from my to-merge list; please ping me again when this is ready.

[ejgallego]

@palmskog , I'm removing the milestone as this is indeed targeting 0.11 which seems incorrect.

I understand the actions here would be:

• when this is ready, create a new milestone for 0.7.x and target this
• release 0.7.x
• create an issue / PR for forward porting to the 0.12 branch. Looks good to you?