diff --git a/.gitignore b/.gitignore index abb79824ca150559cd2c27b63f346649b133544d..813dbb755e55bd230d7e321447418b862e9da259 100644 --- a/.gitignore +++ b/.gitignore @@ -271,7 +271,10 @@ pvsbin/ # Try Why3 /src/trywhy3/trywhy3.js /src/trywhy3/trywhy3.byte -/src/trywhy3/theories.ml +/src/trywhy3/index.en.html +/src/trywhy3/index.fr.html +/src/trywhy3/ace-builds +/src/trywhy3/alt-ergo-0.99.1 # jessie3 /src/jessie/config.log diff --git a/Makefile.in b/Makefile.in index 7dc667926fba974213f1d812ff8e77b3150a7e17..6d4e0e4f608bbdf99d52ee296c1019d7b309b0bb 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1436,6 +1436,14 @@ ALTERGOMODS=util/numbers util/version util/options parsing/why_parser parsing/wh TRYWHY3CMO=lib/why3/why3.cma # $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS))) +trywhy3: src/trywhy3/trywhy3.js src/trywhy3/index.en.html src/trywhy3/index.fr.html + +%.fr.html: %.prehtml + yamlpp -l fr $< -o $@ + +%.en.html: %.prehtml + yamlpp -l en $< -o $@ + src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \ --file=try_alt_ergo.drv:/ \ diff --git a/src/trywhy3/index.html b/src/trywhy3/index.html deleted file mode 100644 index b5b8789376f8f2e4b5439212ae9eb263140b80b8..0000000000000000000000000000000000000000 --- a/src/trywhy3/index.html +++ /dev/null @@ -1,101 +0,0 @@ - - - Try Why3 - - - - - - - - -
-
- The content of the current buffer will be lost.
-
- - -
-
-
- -

Try Why3

-

Type some program in the text area below, then select - 'Prove all' in the Why3 menu to generate proof obligations.

-

Related links -

-

- -
-
-
-
-
- - - - - - diff --git a/src/trywhy3/index.prehtml b/src/trywhy3/index.prehtml new file mode 100644 index 0000000000000000000000000000000000000000..a1b38011d0f86be821f2869a896eb15b7fb6b7ab --- /dev/null +++ b/src/trywhy3/index.prehtml @@ -0,0 +1,169 @@ + + + + <#en>Try Why3</#en><#fr>Essayez Why3</#fr> + + + + + + + + + +
+
+ <#en>The content of the current buffer will be lost + <#fr>Le contenu actuel du programme sera perdu +
+
+ + +
+
+
+ +
+ <#fr>English version + <#en>Version française +
+

+ <#en>Try Why3<#fr>Essayez Why3 +

+

+ <#en> + Type some program in the text area below, then select + 'Prove all' in the Why3 menu to generate proof obligations. + + <#fr> + Tapez un programme dans la zone de texte ci-dessous, puis + sélectionnez 'Prouver' dans le menu Why3 pour engendrer + les obligations de preuve. + +

+

<#en>Related links<#fr>Liens utiles +

+

+ +
+
+
+
+
+ + + + + +