example prover: extraction resurected

.gitignore

@@ -240,10 +240,6 @@ pvsbin/
 /examples/in_progress/binary_search2/
 /examples/in_progress/binary_search_c/
 /examples/in_progress/vacid_0_red_black_trees_harness/
-/examples/in_progress/prover/bench/*/*.out
-/examples/in_progress/prover/bench/*/*.txt
-/examples/in_progress/prover/bench1
-/examples/in_progress/prover/bench2
 /examples/why3bench.html
 /examples/why3regtests.err
 /examples/why3regtests.out
@@ -282,9 +278,13 @@ pvsbin/
 /examples/in_progress/bigInt/*__*.ml
 /examples/in_progress/mp/jsmain.js
 /examples/in_progress/mp/*__*.ml
-/examples/in_progress/prover/build/*__*.ml
-/examples/in_progress/prover/.depend
-/examples/in_progress/prover/build/prover
+/examples/prover/build/*__*.ml
+/examples/prover/.depend
+/examples/prover/build/prover
+/examples/prover/bench/*/*.out
+/examples/prover/bench/*/*.txt
+/examples/prover/bench1
+/examples/prover/bench2
 
 # modules
 /modules/string/

Makefile.in

@@ -651,13 +651,14 @@ gallery-simple::
 
 .PHONY: gallery-subs
 
-GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp
+GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp prover
 
 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 $(GALLERYDIR)/$$d; \
 	  cd examples/$$d; \
 	  why3 -L . doc --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
 	  cd ..; \

examples/prover/Makefile

@@ -2,8 +2,8 @@
 BENCH ?= no
 
 ifeq ($(BENCH),yes)
-  WHY3=../../../bin/why3.opt
-  WHY3SHARE=../../../share
+  WHY3=../../bin/why3.opt
+  WHY3SHARE=../../share
 else
   ifeq ($(BINDIR),)
     WHY3=why3
@@ -37,7 +37,7 @@ MLALL=$(MLUTIL) $(MLTYPES) $(MLIMPL)
 ML=$(patsubst %,%.ml,$(MLALL))
 CMX=$(patsubst %,%.cmx,$(MLALL))
 OCAMLC=ocamlopt.opt
-INCLUDES=-I $(BD) $(INCLUDEALL) -I ../../../plugins/tptp
+INCLUDES=-I $(BD) $(INCLUDEALL) -I ../../plugins/tptp
 LIBS=unix.cmxa nums.cmxa $(BIGINTLIB).cmxa dynlink.cmxa str.cmxa menhirLib.cmx zip.cmxa why3.cmxa why3extract.cmxa tptp_ast.cmx tptp_typing.cmx tptp_parser.cmx tptp_lexer.cmx
 LIBSOLD=$(BD)/why3__BuiltIn.cmx $(BD)/int__Int.cmx $(BD)/array__Array.cmx
 WHY3FLAGS=-L . --debug ignore_unused_vars