release 0.82

CHANGES

@@ -2,8 +2,8 @@
 * marks an incompatible change
 
 
-version 0.82, December 9, 2013
-============================
+version 0.82, December 12, 2013
+===============================
 
   o lemma functions
   o polymorphic recursion permitted
@@ -29,16 +29,17 @@ version 0.82, December 9, 2013
   * [emacs] why.el renamed to why3.el
   * [GTK sourceview] why.lang renamed to why3.lang
   * Loc.try[1-7] functions now take location as an optional parameter
-  * [fix] remove extra leading zeros in decimal literals when a prover don't like them
-  * [fix] PVS output: types are always non-empty
-  * [fix] PVS: fixed configuration and installation process
-  * [fix] Coq tactic: now loads dynamic plug-ins
-  * [fix] bug #15493: correct Coq output for polymorphic algebraic data types
-  * [fix] wish #15053: Remove proof time from "Goals proved by only one prover" section of why3session info --stats
-  * [fix] bug #13736: why3ml was slow when there are many inclusions
-  * [fix] bug #16488: decimals in TPTP syntax
-  * [fix] bug #16454: do not send arithmetic triggers anymore to alt-Ergo
-  * [fix] syntax highlighting bugs: should be fixed by removing the old language
+  o [fix] remove extra leading zeros in decimal literals when a prover don't like them
+  o [fix] PVS output: types are always non-empty
+  o [fix] PVS: fixed configuration and installation process
+  o [fix] Coq tactic: now loads dynamic plug-ins
+  o [fix] bug #15493: correct Coq output for polymorphic algebraic data types
+  * [fix] wish #15053: Remove proof time from "Goals proved by only one prover" section 
+    of why3session info --stats
+  o [fix] bug #13736: why3ml was slow when there are many inclusions
+  o [fix] bug #16488: decimals in TPTP syntax
+  o [fix] bug #16454: do not send arithmetic triggers anymore to alt-Ergo
+  o [fix] syntax highlighting bugs: should be fixed by removing the old language
     file alt-ergo.lang from alt-ergo distribution
 
 version 0.81, March 25, 2013

Makefile.in

@@ -1693,7 +1693,7 @@ DISTRIB_FILES = Version Makefile.in configure.in configure \
       src/*.ml* src/*.dep src/*/*.ml* src/*/*.dep src/*/*.c \
       plugins/printer/.keepme plugins/*/*.ml* plugins/*/*.dep \
       lib/why3/META.in lib/why3/why3.ml \
-      bin/why3-call-pvs \
+      lib/why3-call-pvs \
       doc/version.tex.in doc/manual.pdf \
       drivers/*.drv drivers/*.gen \
       examples/*.mlw examples/logic/*.why \
@@ -1705,11 +1705,17 @@ DISTRIB_FILES = Version Makefile.in configure.in configure \
       examples/foveoos11-cm/*.mlw \
       examples/*/*.xml examples/*/*/*.xml examples/*/*/*/*.xml \
       examples/*/*.v   examples/*/*/*.v examples/*/*/*/*.v\
+      examples/*/*.pvs   examples/*/*/*.pvs examples/*/*/*/*.pvs \
+      examples/*/*.prf   examples/*/*/*.prf examples/*/*/*/*.prf \
+      examples/*/*.thy   examples/*/*/*.thy examples/*/*/*/*.thy \
       examples/use_api/*.ml \
       theories/*.why \
       modules/*.mlw \
       lib/coq/*.v lib/coq/*/*.v lib/coq-tactic/*.v \
       lib/pvs/*/*.pvs lib/pvs/*/*.prf \
+      lib/isabelle/why3.ML lib/isabelle/ROOT lib/isabelle/*.thy \
+      lib/isabelle/etc lib/isabelle/Tools \
+      lib/ocaml/*.ml lib/ocaml/*.dep \
       share/provers-detection-data.conf \
       share/why3session.dtd \
       share/javascript/*.js share/javascript/*.css \
@@ -1754,6 +1760,21 @@ $(DISTRIB_TAR): doc/manual.pdf
           $(COQPGENERATED) $(WHY3DOCGENERATED) $(PLUGGENERATED)
 	cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
 
+
+EXTRA_DIST = configure doc/manual.pdf
+
+dist: $(EXTRA_DIST)
+	rm -rf $(DISTRIB_TAR) $(DISTRIB_DIR)
+	mkdir $(DISTRIB_DIR)
+	for d in `git ls-tree -d -r --name-only HEAD`; do mkdir $(DISTRIB_DIR)/$$d; done
+	for f in `git ls-tree -r --name-only HEAD` $(EXTRA_DIST); do cp $$f $(DISTRIB_DIR)/$$f; done
+	rm `find $(DISTRIB_DIR) -name .gitignore`
+	rm -rf  $(DISTRIB_DIR)/examples/in_progress
+	rm -rf  $(DISTRIB_DIR)/misc
+	cd $(DISTRIB_DIR); rm ROADMAP DEVELOPER.readme
+	cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
+
+
 # distrib export: source export-doc export-www export-examples export-examples-c linux
 #
 # export-www:

ROADMAP

@@ -214,8 +214,8 @@ Scheduled for 9 december 2013
 * 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"
-* manual in HTML: "make doc/html/index.html"
-* do "make distrib"
+  (check that manual in HTML is also generated, doc/html/index.html)
+* do "make dist"
 * test distrib/why3-0.82.tar.gz
 * install web page for why2 which includes an updated page for the
   quick migration guide. (sources are in CVS repository
@@ -245,7 +245,7 @@ Scheduled for 9 december 2013
     rm /users/www-perso/projets/why3/api
     ln -s /users/www-perso/projets/why3/api-0.82 \
       /users/www-perso/projets/why3/api
-   PROBLEME avec style.css
+   (PROBLEME avec style.css ? Ou est le probleme ?)
  - update the main HTML page (sources are in repository why3-www)
    edit index.html
    make export