The proof obligations for each prover are generated only as temporary files by why3, so making them available would require significant changes.
By more importantly: I guess you are mainly interested in the case where your favorite prover failed to prove the VC, right ? But then we usually do not keep that in the proof session, so you wouldn't have them anyway in the gallery.
I'm afraid that to get the failing VCs, there is no simpler way than taking the example file and session, and replay them with why3
Maybe the best way to do such a task would be with a short Ocaml program linked with why3.cma, as examplified by examples distributed in examples/use_api/
- Claude Le 02/09/2014 15:33, Mohamed Iguernelala a écrit :
Hi JC, It's interesting to have a "Why3 Proof Results for Project ...." at the end of each (html) report. But, is it possible/easy to enrich these html files with links to the proof obligations generated for each prover ? - Mohamed.
-- Claude Marché | tel: +33 1 72 92 59 69 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
