Commit 89c38c59 authored by MARCHE Claude's avatar MARCHE Claude

Ceci n'est pas un message de commit

parent 4c763af2
......@@ -120,6 +120,7 @@ why3.conf
/src/*.a
# Coq tactic
/src/coq-tactic/coqCompat.ml
/src/coq-tactic/g_why3tac.ml
/src/coq-tactic/.why3-vo-*
/lib/coq-tactic/why3tac.cma
......
* marks an incompatible change
o [Provers] support for Coq 8.4
o New scheme for Coq realizations, using type classes
version 0.73, Jul 19, 2012
==========================
o [IDE] "Clean" was cleaning too much
* no more executable why3ml (why3 now handles WhyML files)
o [Provers] support for Z3 4.0
......
......@@ -121,22 +121,27 @@ scheduled on Sep 2012
== New Features to announce ==
New features:
o
o Support for Coq 8.4
o dropped support for Coq 8.2
o new scheme for Coq realizations using type classes
o new API for programs
o Support for PVS 6.0
Bug fix:
Bug fixes:
o
== Final preparation ==
* do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK
* check that "make xml-validate" is OK
* put 0.74 in file Version
* check headers
* check the file CHANGES
* check the file CHANGES, add the release date
* manual in PDF: check that macro \todo is commented out
in ./macros.tex, and then "make doc"
* do "make distrib"
* test the distrib why3-0.73.tar.gz
* test the distrib why3-0.74.tar.gz
* make a last commit:
- add tag 0.74 to the git repository
- do not forget to push it using git push --tags
......@@ -157,7 +162,7 @@ Bug fix:
- update the main HTML page (sources are in why3-papers/www)
* produce the Why3 part of ProVal gallery
-> add also a ZIP file of it
-> add also a tar.gz and a ZIP file of it
* Announce the distrib
- What to put in the announcement: see New Features above
* The next commit : add +git to the version in file Version
......@@ -167,7 +172,7 @@ Bug fix:
* Sortie PVS
** avec mecanisme de realization
* Yices 2 ? interesserait Cesar
* support de Yices 2 ? interesserait Cesar
* mettre au propre les loc des fichiers de sessions, en particulier
les noms de fichiers doivent etre relatifs au fichier de session
......@@ -183,14 +188,14 @@ Bug fix:
- (CLAUDE) complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
* PRIORITAIRE Coq output
* DONE (PRIORITAIRE) Coq output
- corriger l'incoherence, comprendre si on veut vraiment accepter
function x : 'a
(cf: en caml cela ne marche pas)
Solution proposee: utiliser des types classes, en particulier Inhabited
* PRIORITAIRE, JCF et ANDREI, clone de module
* DONE ? PRIORITAIRE, JCF et ANDREI, clone de module
- demarche: ecrire une API avec smart constructors garantissant
le bon typage, et clone sera en premier lieu un de ces constructors
- cas d'utilisation: range d'entiers de Jessie, Flottants -> double ou single
......
......@@ -267,6 +267,7 @@ name = "Coq"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.4"
version_ok = "8.3pl4"
version_ok = "8.3pl3"
version_ok = "8.3pl2"
......@@ -276,20 +277,6 @@ command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3
driver = "drivers/coq.drv"
editor = "coqide"
[ITP coq]
name = "Coq"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_old = "8.2pl2"
version_old = "8.2pl1"
version_old = "8.2"
version_old = "8.1"
version_old = "8.0"
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv"
editor = "coqide"
[ITP pvs]
name = "PVS"
exec = "pvs"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment