Permalink
Browse files

Tentative and very experminental support for typerex. Enabled with

./configure -typerex .

It causes (non-fatal) errors when compiling files without a .mli (the problem
seems to have something to do with the flag -intf-suffix .cmi).

In practice, most typerex functionalities don't work well because typerex
fails its lookup into files compiled with -rectypes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15302 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 2abc6e4 commit 5ea279dbd47d9ef1b87351e4df469aba3310f3f0 @aspiwack aspiwack committed May 11, 2012
Showing with 27 additions and 2 deletions.
  1. +18 −0 .typerex
  2. +2 −2 Makefile.build
  3. +1 −0 config/Makefile.template
  4. +6 −0 configure
View
@@ -0,0 +1,18 @@
+parsing
+ide
+ide/utils
+interp
+kernel
+kernel/byterun
+lib
+library
+plugins
+pretyping
+proofs
+scripts
+states
+tactics
+theories
+tools
+tools/coqdoc
+toplevel
View
@@ -83,8 +83,8 @@ HIDE := $(if $(VERBOSE),,@)
LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
-OCAMLC += $(CAMLFLAGS)
-OCAMLOPT += $(CAMLFLAGS)
+OCAMLC := $(TYPEREX) $(OCAMLC) $(CAMLFLAGS)
+OCAMLOPT := $(TYPEREX) $(OCAMLOPT) $(CAMLFLAGS)
BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
@@ -83,6 +83,7 @@ CAMLMKTOP="CAMLMKTOPEXEC"
# Caml flags
CAMLFLAGS=-rectypes CAMLANNOTATEFLAG
+TYPEREX=TYPEREXCMD
# Compilation debug flags
CAMLDEBUG=COQDEBUGFLAG
View
@@ -93,6 +93,8 @@ usage () {
printf "\tAdd profiling information in the Coq executables\n"
echo "-annotate"
printf "\tCompiles Coq with -dtypes option\n"
+ echo "-typerex"
+ printf "\tCompiles Coq using typerex wrapper\n"
echo "-makecmd <command>"
printf "\tName of GNU Make command.\n"
}
@@ -109,12 +111,14 @@ ocamllexexec=ocamllex
ocamlyaccexec=ocamlyacc
ocamlmktopexec=ocamlmktop
camlp4oexec=camlp4o
+default_typerex_wrapper="ocp-wrapper -save-types"
coq_debug_flag=
coq_debug_flag_opt=
coq_profile_flag=
coq_annotate_flag=
+coq_typerex_wrapper=
best_compiler=opt
cflags="-fno-defer-pop -Wall -Wno-unused"
natdynlink=yes
@@ -272,6 +276,7 @@ while : ; do
-debug|--debug) coq_debug_flag=-g;;
-profile|--profile) coq_profile_flag=-p;;
-annotate|--annotate) coq_annotate_flag=-dtypes;;
+ -typerex|--typerex) coq_typerex_wrapper=$default_typerex_wrapper;;
-force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version)
force_caml_version_spec=yes
force_caml_version=yes;;
@@ -1157,6 +1162,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|COQDEBUGFLAG|$coq_debug_flag|" \
-e "s|COQPROFILEFLAG|$coq_profile_flag|" \
-e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \
+ -e "s|TYPEREXCMD|$coq_typerex_wrapper|" \
-e "s|CCOMPILEFLAGS|$cflags|" \
-e "s|BESTCOMPILER|$best_compiler|" \
-e "s|DLLEXTENSION|$DLLEXT|" \

0 comments on commit 5ea279d

Please sign in to comment.