Commit a8e60ac6 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Merge branch 'next' into new_ide

parents 93fcceb1 9c606eb7
:x: marks a potential source of incompatibility
Version 0.88.2, December 7, 2017
--------------------------------
Bug fixes
* `why3 session html`: improved compliance of generated files
* `why3 doc`: fixed missing anchors for operator definitions
* improved build process when `coqtop.byte` is missing
Version 0.88.1, November 6, 2017
--------------------------------
......@@ -8,7 +16,7 @@ API
Provers
* improved support for Isabelle 2017
* fixed support for Coq 8.7
* fixed support for Coq 8.7 (released Oct 17, 2017)
Miscellaneous
* fixed compilation for OCaml 4.06
......@@ -34,16 +42,16 @@ Standard library
compliant to IEEE-754, mapped to SMT-LIB FP theory.
User features
* proof strategies: why3 config now generates default proof strategies
* proof strategies: `why3 config` now generates default proof strategies
using the installed provers. These are available under name "Auto
level 0", "Auto level 1" and "Auto level 2" in why3 ide.
level 0", "Auto level 1" and "Auto level 2" in `why3 ide`.
More details in the manual, section 10.6 "Proof Strategies".
* counterexamples: better support for array values, support for
floating-point values, support for Z3 in addition to CVC4.
More details in the manual, section 6.3.5 "Displaying Counterexamples".
Provers
* support for Isabelle 2017
* support for Isabelle 2017 (released Oct 2017)
* discarded support for Isabelle 2016 (2016-1 still supported) :x:
* support for Coq 8.6.1 (released Jul 25, 2017)
* tentative support for Coq 8.7
......@@ -89,7 +97,7 @@ Language
Tools
* added a command-line option `--extra-expl-prefix` to specify
additional possible prefixes for VC explanations. Available for
why3 commands `prove` and `ide`.
`why3` commands `prove` and `ide`.
* removed `jstree` style from the `session` command :x:
Transformations
......@@ -158,7 +166,7 @@ Provers
* support for Gappa 1.2 (released May 19, 2015)
Bug fixes
* why3doc: garbled output
* `why3doc`: garbled output
Version 0.86, May 11, 2015
--------------------------
......
......@@ -299,10 +299,13 @@ GENERATED += $(LIBGENERATED)
clean_old_install::
rm -rf $(LIBDIR)/why3
rm -rf $(DATADIR)/why3
rm -rf $(OCAMLINSTALLLIB)/why3
clean_old_install-lib::
if test -d $(OCAMLINSTALLLIB) -a -w $(OCAMLINSTALLLIB); then \
rm -f $(OCAMLINSTALLLIB)/why3; \
fi
install_no_local:: clean_old_install
install_no_local::
$(MKDIR_P) $(BINDIR)
$(MKDIR_P) $(LIBDIR)/why3
$(MKDIR_P) $(TOOLDIR)
......@@ -345,7 +348,7 @@ install install-lib:
@echo "To install Why3, run ./configure --disable-local ; make ; make install"
else
install: clean_old_install install_no_local
install-lib: install_no_local_lib
install-lib: clean_old_install-lib install_no_local_lib
endif
install-all: install install-lib
......@@ -354,7 +357,12 @@ install-all: install install-lib
# Uninstallation
##################
uninstall: clean_old_install
ifeq (@enable_local@,yes)
uninstall:
@echo "Why3 is configured in local installation mode."
else
uninstall: clean_old_install clean_old_install-lib
endif
##################
# Why3 emacs mode
......@@ -667,7 +675,6 @@ gallery-subs::
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
@for d in $(GALLERYSUBS) ; do \
echo "exporting examples/$$d"; \
rm -f $(GALLERYDIR)/$$d/$$d.zip; \
mkdir -p $(GALLERYDIR)/$$d; \
cd examples/$$d; \
WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../theories -L ../../modules -L . --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
......@@ -684,7 +691,7 @@ gallery-subs::
d=`dirname $$x`; \
f=`basename $$d`; \
echo "exporting $$f"; \
rm $$d/*.bak; \
rm -f $$d/*.bak; \
mkdir -p $(GALLERYDIR)/$$f; \
WHY3CONFIG="" bin/why3session.@OCAMLBEST@ html $$d -o $(GALLERYDIR)/$$f; \
if test -f examples/$$f.mlw; then cp examples/$$f.mlw $(GALLERYDIR)/$$f/; fi; \
......@@ -1942,10 +1949,6 @@ doc/apidoc/dg.svg: doc/apidoc/dg.dot
doc/apidoc/dg.png: doc/apidoc/dg.dot
dot -T png $< > $@
# what is this ? api doc is in why3.lri.fr/api instead...
# install_apidoc: apidoc
# rsync -av doc/apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/
doc/apidoc.tex: $(FILESTODOC)
$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
$(LIBINCLUDES) -I lib/why3 $(FILESTODOC)
......@@ -1954,11 +1957,13 @@ clean::
rm -f doc/apidoc/*
##########
# Install rules that require root, and thus appear last in the file!
# Install rules for bash completions
##########
clean_old_install::
if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then rm -f /etc/bash_completion.d/why3; fi
if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
rm -f /etc/bash_completion.d/why3; \
fi
install_no_local::
if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \
......
......@@ -121,7 +121,7 @@
* check/update the content of the About dialog in src/ide/gconfig.ml
around lines 550-600
* check headers
* check the file CHANGES, add the release date
* check the file CHANGES.md, add the release date
* generate documentation
- update the date in doc/manual.tex (near \whyversion{})
......@@ -158,9 +158,6 @@
- make (to check validity)
- make export
* add a new version to the bugtracker:
https://gforge.inria.fr/tracker/admin/?group_id=2990&atid=10293&add_extrafield=1
* The next commit : add +git to the version in file Version
* prepare the OPAM package
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, November 2017
Version \whyversion{}, December 2017
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
......@@ -62,4 +62,5 @@ conflicts: [
"lablgtk" {< "2.14.2"}
"ocamlgraph" {< "1.8.2"}
"coq" {< "8.4"}
"coq" {>= "8.8"}
]
......@@ -23,7 +23,7 @@ tags: [
]
available: [ ocaml-version >= "4.02.3" & ocaml-version < "4.06" ]
depends: [
"why3-base" { = "0.88.1" }
"why3-base" { = "0.88.2" }
"lablgtk"
"conf-gtksourceview"
"zarith"
......
......@@ -998,8 +998,12 @@ lident_rich:
| lident_op_id { $1 }
lident_op_id:
| LEFTPAR lident_op RIGHTPAR { mk_id $2 $startpos $endpos }
| LEFTPAR_STAR_RIGHTPAR { mk_id (infix "*") $startpos $endpos }
| LEFTPAR lident_op RIGHTPAR { mk_id $2 $startpos($2) $endpos($2) }
| LEFTPAR_STAR_RIGHTPAR
{ (* parentheses are removed from the location *)
let s = let s = $startpos in { s with pos_cnum = s.pos_cnum + 1 } in
let e = let e = $endpos in { e with pos_cnum = e.pos_cnum - 1 } in
mk_id (infix "*") s e }
lident_op:
| op_symbol { infix $1 }
......
......@@ -13,7 +13,12 @@ open Why3
open Ident
let stdlib_url = ref None
let set_stdlib_url u = stdlib_url := Some u
let set_stdlib_url u =
let u =
let l = String.length u in
if l = 0 || u.[l - 1] = '/' then u
else u ^ "/" in
stdlib_url := Some u
let output_dir = ref None
let set_output_dir d = output_dir := d
......@@ -59,7 +64,7 @@ let pp_url fmt lp =
let fn = String.concat "." lp in
match !stdlib_url with
| Some www when not (is_local_file fn) ->
Format.fprintf fmt "%s/%s.html" www fn
Format.fprintf fmt "%s%s.html" www fn
| _ ->
Format.fprintf fmt "%s.html" fn
......
......@@ -51,15 +51,18 @@
let current_file = ref ""
let print_ident fmt lexbuf s =
let print_ident ?(parentheses=false) fmt lexbuf s =
if is_keyword1 s then
fprintf fmt "<span class=\"keyword1\">%s</span>" s
else if is_keyword2 s then
fprintf fmt "<span class=\"keyword2\">%s</span>" s
else begin
let (* f,l,c as *) loc = get_loc lexbuf in
(* Format.eprintf " IDENT %s/%d/%d@." f l c; *)
(* is this a def point? *)
let loc =
let loc = get_loc lexbuf in
if parentheses then
let (f,l,s,e) = Loc.get loc in
Loc.user_position f l (s + 1) (e - 1)
else loc in
try
let id, def = Glob.find loc in
match id.Ident.id_loc with
......@@ -107,8 +110,9 @@ let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* | operator
let special = ['\'' '"' '<' '>' '&']
rule scan fmt empty = parse
| "(*)" as s
{ pp_print_string fmt s;
| "(*)" { pp_print_char fmt '(';
print_ident ~parentheses:true fmt lexbuf "*";
pp_print_char fmt ')';
scan fmt NotEmpty lexbuf }
| space* "(***"
{ comment fmt false lexbuf;
......
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