Commit d02aed18 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'bugfix/v0.88' into next

parents 2ffa2632 2fe582c8
.gitattributes export-ignore
.gitignore export-ignore
.keepme export-ignore
/.gitlab-ci.yml export-ignore
/.mailmap export-ignore
......
......@@ -2,21 +2,21 @@
Provers
* support for Alt-Ergo 2.0.0 (released Nov 14, 2017)
* support for Coq 8.7.1 (released Dec 16, 2017)
* support for Z3 4.6.0 (released Dec 18, 2017)
Standard library
* fix compatibility of theory int.Exponentiation with instances
where multiplication is not commutative.
fix corresponding realizations in Coq and Isabelle/HOL :x:
* fixed soundness of theory `int.Exponentiation` when multiplication is not
commutative :x:
Bug fixes
* Fix issue #50:
share/Makefile.config is missing when enable_relocation=yes
Miscellaneous
* fixed support for `--enable_relocation=yes` (issue #50)
* fixed support for Windows (issue #70)
Version 0.88.2, December 7, 2017
--------------------------------
Bug fixes
Miscellaneous
* `why3 session html`: improved compliance of generated files
* `why3 doc`: fixed missing anchors for operator definitions
* improved build process when `coqtop.byte` is missing
......
......@@ -441,45 +441,27 @@ LIBPLUGCMXS = $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))
plugins.byte: $(LIBPLUGCMO)
plugins.opt : $(LIBPLUGCMXS)
lib/plugins/%.cmxs: plugins/parser/%.cmx
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
lib/plugins:
mkdir lib/plugins
lib/plugins/%.cmo: plugins/parser/%.cmo
lib/plugins/%.cmxs: | lib/plugins
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
lib/plugins/%.cmxs: plugins/printer/%.cmx
lib/plugins/%.cmo: | lib/plugins
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/plugins/%.cmxs: plugins/parser/%.cmx
lib/plugins/%.cmo: plugins/parser/%.cmo
lib/plugins/%.cmxs: plugins/printer/%.cmx
lib/plugins/%.cmo: plugins/printer/%.cmo
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
lib/plugins/%.cmxs: plugins/transform/%.cmx
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
lib/plugins/%.cmo: plugins/transform/%.cmo
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
lib/plugins/tptp.cmxs: $(TPTPCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
lib/plugins/tptp.cmo: $(TPTPCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/plugins/python.cmxs: $(PYTHONCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
lib/plugins/python.cmo: $(PYTHONCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
# depend and clean targets
......@@ -521,6 +503,9 @@ $(TOOLSDEP): $(TOOLSGENERATED)
byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.byte)
opt: bin/why3.opt $(TOOLS_BIN:%=bin/%.opt)
bin:
mkdir bin
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
bin/why3.byte: lib/why3/why3.cma src/tools/main.cmo
bin/why3config.opt: lib/why3/why3.cmxa src/tools/why3config.cmx
......@@ -734,14 +719,10 @@ opt: bin/why3ide.opt
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
bin/why3ide.byte: BLINKFLAGS += -custom
bin/why3ide.opt: lib/why3/why3.cmxa src/ide/resetgc.o $(IDECMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3ide.byte: lib/why3/why3.cma src/ide/resetgc.o $(IDECMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
src/ide/resetgc.o: src/ide/resetgc.c
$(SHOW) 'Ocamlc $<'
......@@ -791,12 +772,7 @@ byte: bin/why3session.byte
opt: bin/why3session.opt
bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
......@@ -1469,12 +1445,7 @@ byte: bin/why3doc.byte
opt: bin/why3doc.opt
bin/why3doc.opt: lib/why3/why3.cmxa $(WHY3DOCCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3doc.byte: lib/why3/why3.cma $(WHY3DOCCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
......@@ -1970,11 +1941,11 @@ src/tools/why3extract.cmx src/ide/gmain.cmx: %.cmx: %.ml
echo '$*.cmx : $*.cmi'; \
echo '$*.cmi : $*.cmo') $(TOTARGET)
%.opt:
bin/%.opt: | bin
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
%.byte:
bin/%.byte: | bin
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
......
......@@ -528,6 +528,7 @@ compile_time_support = true
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.7.1"
version_ok = "8.7.0"
version_ok = "8.6.1"
version_ok = "8.6"
......
......@@ -991,8 +991,8 @@ lident_op_id:
| 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
let s = let s = $startpos in { s with Lexing.pos_cnum = s.Lexing.pos_cnum + 1 } in
let e = let e = $endpos in { e with Lexing.pos_cnum = e.Lexing.pos_cnum - 1 } in
mk_id (infix "*") s e }
lident_op:
......
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