Open xldenis opened 5 months ago
I suggest we focus in this issue on why3find (the binary builds can be a separate issue) :). In the meeting this morning we discussed the following approach for testing/adopting why3find progressively:
cargo creusot
user workflow. We'll probably want to replace the cargo creusot why3 prove
subcommand to use why3find.@xldenis could you describe here the rough steps you had to follow to use why3find with creusot, so that we can reproduce it on our side, and work on the integration with the testsuite?
Commands to run why3find
on all the tests (the long flag is just to turn off warnings to make the logs are more readable):
why3find config --detect --why3-warn-off unused_variable,axiom_abstract -j 8
why3find prove creusot/tests
There was a wrinkle with an old test file, which is fixed by #1147.
Ignoring the tests whose proofs we don't care about, the following test cases could not be verified by why3find prove
:
why3find prove creusot/tests/should_succeed/iterators/04_skip.coma
why3find prove creusot/tests/should_succeed/iterators/05_map.coma
why3find prove creusot/tests/should_succeed/iterators/06_map_precond.coma
why3find prove creusot/tests/should_succeed/iterators/12_zip.coma
why3find prove creusot/tests/should_succeed/iterators/15_enumerate.coma
why3find prove creusot/tests/should_succeed/iterators/16_take.coma
why3find prove creusot/tests/should_succeed/iterators/17_filter.coma
why3find prove creusot/tests/should_succeed/sparse_array.coma
why3find prove creusot/tests/should_succeed/syntax/derive_macros/mixed.coma
why3find prove creusot/tests/should_succeed/vector/06_knights_tour.coma # fixed in #1150 (iterator shenanigans)
why3find prove creusot/tests/should_succeed/list_reversal_lasso.coma # fixed with longer timeout and option --tactic +inline_goal,+split_all_full
why3find prove creusot/tests/should_succeed/sum.coma # fixed with longer timeout and option --tactic +inline_goal
why3find prove creusot/tests/should_succeed/bdd.coma # fixed by a longer timeout
why3find prove creusot/tests/should_succeed/hashmap.coma # fixed by a longer timeout
why3find prove creusot/tests/should_succeed/heapsort_generic.coma # fixed by adding cvc
why3find prove creusot/tests/should_succeed/iterators/03_std_iterators.coma # fixed by adding cvc
why3find prove creusot/tests/should_succeed/iterators/10_once.coma # fixed by a longer timeout
why3find prove creusot/tests/should_succeed/red_black_tree.coma # fixed by adding cvc
why3find prove creusot/tests/should_succeed/selection_sort_generic.coma # fixed by a longer timeout
why3find prove creusot/tests/should_succeed/vector/08_haystack.coma # fixed by adding cvc
Why3 Find is finally public: https://git.frama-c.com/pub/why3find. We should integrate this into creusot to ship a complete CLI driven workflow for verification. Once we have this we should also start producing nightly binary builds of a complete creusot install to make setup 100% seamless.