Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Work around for a bug with the Why3 back-end of Jessie

  • Subject: [Frama-c-discuss] Work around for a bug with the Why3 back-end of Jessie
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Wed, 22 Aug 2012 17:54:17 +0200
With the combination of Why3 0.73 and Why 2.31 that were released last 
July, there is a bug that prevents Why3 from running if the Coq prover 
is *not* installed.

This can be fixed by editing the file

WHYLIB/why3/why3.conf

(typically WHYLIB = /usr/local/lib/why)

and removing the [prover coq] section (3 lines)

- Claude

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