Stream: CUDW 2020

Topic: fix simpl


view this post on Zulip Yves Bertot (Dec 03 2020 at 11:09):

This makes me mad. I modified the simpl tactic, and in the CI coq now fails on "performance tests". I would be happy to fix the problem in performance test, but understanding what these file do is a pain.

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 11:11):

ci link?

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 11:13):

@Yves Bertot : are you working on simpl or cbn? Isn't simpl deprecated?

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 11:13):

it is not

view this post on Zulip Yves Bertot (Dec 03 2020 at 11:14):

The error message is a very informative "Error: Tactic failure: time_solve_goal failed!."

view this post on Zulip Yves Bertot (Dec 03 2020 at 11:15):

@Michael Soegtrop simpl is used extensively in math-comp and cbn does not provide a viable alternative, according to discussion in issue #13428.

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 11:16):

Yves Bertot said:

The error message is a very informative "Error: Tactic failure: time_solve_goal failed!."

link to full log please

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 11:17):

It would be good to have a discription of what cbn and simpl do for users. I have a lot of issues with both in VST. Usually cbn behaves better in the sense that it doesn't reduce to deeply, but not always.

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 11:18):

If only I knew...

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 11:21):

You mean I have to reconstruct some lost lore from the sources to know what simpl does?

view this post on Zulip Yves Bertot (Dec 03 2020 at 11:21):

This is the reason I decided to spend some time on it. First fix a behavior that is agreed to be wrong, then acquire a little more knowledge about the specification and actual behavior.

view this post on Zulip Michael Soegtrop (Dec 03 2020 at 11:26):

That would indeed be very useful. I guess for cbn the situation is better and it is known what it is supposed to do?

view this post on Zulip Paolo Giarrusso (Dec 03 2020 at 11:49):

Also no

view this post on Zulip Paolo Giarrusso (Dec 03 2020 at 11:51):

There are lots of issues on both on github, and IIUC cbn was a project by a PhD student who left, so nobody understands the new code?

view this post on Zulip Yves Bertot (Dec 03 2020 at 11:58):

If I remember well, for simpl the problem is that the value of a recursive function (when not applied to arguments) is not itself, but a fix expression whose text is the whole code of the recursive function. So the initial design goal for simpl was simply to make sure that occurrences of the fix expression would be re-folded back into the constant of the initial definition.

view this post on Zulip Yves Bertot (Dec 03 2020 at 11:59):

But that is not so simple, because sometimes it is not easy to find the corresponding refolded expression, and there was a need for heuristics. As soon as one is using heuristics, it is difficult to explain.

view this post on Zulip Paolo Giarrusso (Dec 03 2020 at 12:01):

BTW, there was a proposal (from Hugo) to change the fix representation directly, tho I’m sure that’s very invasive

view this post on Zulip Yves Bertot (Dec 03 2020 at 12:26):

Anyway, I am currently having a headache trying to understand what is happening in coq-performance-tests.

view this post on Zulip Enrico Tassi (Dec 03 2020 at 12:36):

@Jason Gross probably knows better what is in that job

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 13:11):

Feel free to ping him in the PR instead of trying to fix it yourself.

view this post on Zulip Yves Bertot (Dec 03 2020 at 13:12):

Okay, I finally figured out that my fix for simpl is changing the behaviour of cbn.

view this post on Zulip Yves Bertot (Dec 03 2020 at 13:49):

According to the documentation, my fix for simpl should change the behaviour of cbn, because both simpl and cbn should respect the simpl never directive when it is used.

view this post on Zulip Yves Bertot (Dec 03 2020 at 13:58):

It so happens that the sieve_of_eratosthenes example in https://github.com/coq-community/coq-performance-tests does rely on on expanding Pos.to_nat, which is contrary to the directive placed at https://github.com/coq/coq/blob/a88568e751d63d8db93450213272c8b28928dbf2/theories/PArith/BinPosDef.v#L544

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 14:07):

Then, it makes sense to prepare an overlay for this project.

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 14:07):

Or to ask the maintainer to do it.

view this post on Zulip Yves Bertot (Dec 03 2020 at 14:09):

Yep, I am doing it. Is there a documentation somewhere about what an overlay is?

view this post on Zulip Yves Bertot (Dec 03 2020 at 14:11):

What I have is more a patch to coq-performance-tests that is hoped to be backward compatible.

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 14:22):

https://github.com/coq/coq/blob/master/dev/ci/user-overlays/README.md

view this post on Zulip Yves Bertot (Dec 03 2020 at 14:30):

Thanks Gaëtan

view this post on Zulip Jason Gross (Dec 03 2020 at 15:43):

Sorry coq-performance-tests is hard to debug. In general the thing to do is, e.g., if PerformanceExperiments/foo/_n_*.v is failing, to open up PerformanceExperiments/foo.v and stick something like Goal True. run<n> Sanity. (or run<n> SuperFast. at the bottom), and debug that

view this post on Zulip Jason Gross (Dec 03 2020 at 15:45):

In any case, we issue Global Arguments Pos.to_nat !_ / . in sieve_of_eratosthenes.v, which should override the simpl never directive in the stdlib, no?

view this post on Zulip Yves Bertot (Dec 04 2020 at 11:47):

@Jason Gross thanks for your help. Your test was actually showing a bug in my implementation, which @Pierre-Marie Pédrot had already spotted directly by scrutiny of the code. This is good, this what tests are for. The inaccuracy of the error message forced me to understand what each of the tactics was doing.

view this post on Zulip Jason Gross (Dec 04 2020 at 15:59):

Indeed, the inaccurate error messages are unfortunate. Unfortunately Ltac doesn't really provide a facility for passing through error messages, nor for raising the failure level of a given error message. Hence it's quite hard to set things up to give the right error messages. Hopefully when Ltac2 becomes sufficiently standard and I port the tests to Ltac2, I'll be able to make use of proper handling of error messages to give more informative ones. It's possible I could hack a better error message in this particular case by sticking a || fail 3 "not equal:" n n' after the constr_eq in https://github.com/coq-community/coq-performance-tests/blob/77fb88a14c014ad9645588a66b65fc8523681ed1/PerformanceExperiments/sieve_of_eratosthenes.v#L44, but I'm not even sure if the right number here is 2 or 3 (I can't recall whether + decreases failure level by 1 or not)


Last updated: Oct 16 2021 at 07:02 UTC