aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend4
-rw-r--r--Makefile62
-rw-r--r--config/coq_config.mli3
-rwxr-xr-xconfigure101
-rw-r--r--distrib/Makefile8
-rw-r--r--lib/options.ml2
-rw-r--r--lib/options.mli2
-rw-r--r--scripts/coqc.ml5
-rw-r--r--toplevel/coqinit.ml24
-rw-r--r--toplevel/coqtop.ml3
-rw-r--r--toplevel/usage.ml1
11 files changed, 98 insertions, 117 deletions
diff --git a/.depend b/.depend
index 13b4364e1..3e8912f29 100644
--- a/.depend
+++ b/.depend
@@ -898,8 +898,8 @@ proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \
proofs/proof_trees.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi
proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx parsing/printer.cmx \
proofs/proof_trees.cmx proofs/tacmach.cmx proofs/tactic_debug.cmi
-scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi
-scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx
+scripts/coqc.cmo: config/coq_config.cmi lib/options.cmi toplevel/usage.cmi
+scripts/coqc.cmx: config/coq_config.cmx lib/options.cmx toplevel/usage.cmx
scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo
scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx
tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \
diff --git a/Makefile b/Makefile
index c0b42ced1..5bb29ce87 100644
--- a/Makefile
+++ b/Makefile
@@ -37,11 +37,11 @@ noargument:
# Compilation options
###########################################################################
-LOCALINCLUDES= -I config -I tools -I scripts -I lib -I kernel -I library \
- -I proofs -I tactics -I pretyping -I parsing -I toplevel \
- -I contrib/omega -I contrib/ring -I contrib/xml \
- -I contrib/extraction -I contrib/correctness \
- -I contrib/interface
+LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
+ -I proofs -I tactics -I pretyping -I parsing -I toplevel \
+ -I contrib/omega -I contrib/ring -I contrib/xml \
+ -I contrib/extraction -I contrib/correctness \
+ -I contrib/interface
INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB)
@@ -55,12 +55,7 @@ OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS)
CAMLP4EXTENDFLAGS=-I . pa_extend.cmo q_MLast.cmo
CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p'
-COQINCLUDES=-I states -R theories Coq -R contrib Coq
-# -I contrib/omega -I contrib/ring -I contrib/xml \
-# -I theories/Init -I theories/Logic -I theories/Arith \
-# -I theories/Bool -I theories/Zarith -I theories/Lists \
-# -I theories/Sets -I theories/Relations -I theories/Wellfounded \
-# -I theories/Reals
+COQINCLUDES=-R theories Coq -R contrib Coq
###########################################################################
# Objects files
@@ -215,12 +210,12 @@ CMX=$(CMO:.cmo=.cmx)
# Main targets (coqmktop, coqtop.opt, coqtop.byte)
###########################################################################
-COQMKTOP=bin/coqmktop
-COQC=bin/coqc
-COQTOPBYTE=bin/coqtop.byte
-COQTOPOPT=bin/coqtop.opt
-BESTCOQTOP=bin/coqtop.$(BEST)
-COQINTERFACE=bin/coq-interface bin/parser
+COQMKTOP=bin/coqmktop$(EXE)
+COQC=bin/coqc$(EXE)
+COQTOPBYTE=bin/coqtop.byte$(EXE)
+COQTOPOPT=bin/coqtop.opt$(EXE)
+BESTCOQTOP=bin/coqtop.$(BEST)$(EXE)
+COQINTERFACE=bin/coq-interface$(EXE) bin/parser
COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQINTERFACE)
@@ -307,7 +302,7 @@ states: states/barestate.coq states/initial.coq
SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v syntax/PPTactic.v
states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP)
- $(BESTCOQTOP) -q -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq
+ $(BESTCOQTOP) -boot -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq
INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \
theories/Init/DatatypesSyntax.vo theories/Init/Prelude.vo \
@@ -317,7 +312,7 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \
theories/Init/Logic_TypeSyntax.vo
theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC)
- $(COQC) -$(BEST) -bindir bin -q -R theories Coq -is states/barestate.coq $<
+ $(COQC) -boot -$(BEST) $(INCLUDES) -R theories Coq -is states/barestate.coq $<
init: $(INITVO)
@@ -328,13 +323,13 @@ TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo \
tactics/EqDecide.vo $(EXTRACTIONVO)
tactics/%.vo: tactics/%.v states/barestate.coq $(COQC)
- $(COQC) -$(BEST) -bindir bin -q -I tactics -is states/barestate.coq $<
+ $(COQC) -boot -$(BEST) $(INCLUDES) -I tactics -is states/barestate.coq $<
contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC)
- $(COQC) -$(BEST) -bindir bin -q -I contrib/extraction -is states/barestate.coq $<
+ $(COQC) -boot -$(BEST) $(COQINCLUDES) -is states/barestate.coq $<
states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO) $(BESTCOQTOP)
- $(BESTCOQTOP) -q -batch -silent -is states/barestate.coq -I tactics -R theories Coq -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
+ $(BESTCOQTOP) -boot -silent -is states/barestate.coq $(COQINCLUDES) $(INCLUDES) -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
clean::
rm -f states/*.coq
@@ -467,10 +462,10 @@ XMLVO = contrib/xml/Xml.vo
INTERFACEV0 = contrib/interface/Centaur.vo
contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
- $(COQC) -q -byte -bindir bin $(COQINCLUDES) $<
+ $(COQC) -boot -byte $(COQINCLUDES) $<
-contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE)
- $(COQC) -q -byte -bindir bin $(COQINCLUDES) $<
+contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq
+ $(COQC) -boot -byte $(COQINCLUDES) $<
CONTRIBVO = $(OMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) $(CORRECTNESSVO)\
$(INTERFACEV0)
@@ -494,13 +489,12 @@ archclean::
# tools
###########################################################################
-COQDEP=bin/coqdep
-COQMAKEFILE=bin/coq_makefile
-GALLINA=bin/gallina
-COQTEX=bin/coq-tex
+COQDEP=bin/coqdep$(EXE)
+COQMAKEFILE=bin/coq_makefile$(EXE)
+GALLINA=bin/gallina$(EXE)
+COQTEX=bin/coq-tex$(EXE)
-tools: $(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) \
- tools/coq.elc dev/top_printers.cmo
+tools: $(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) dev/top_printers.cmo
COQDEPCMO=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo
@@ -536,7 +530,7 @@ MINICOQCMO=$(CONFIG) $(LIB) $(KERNEL) \
parsing/lexer.cmo parsing/g_minicoq.cmo \
toplevel/fhimsg.cmo toplevel/minicoq.cmo
-MINICOQ=bin/minicoq
+MINICOQ=bin/minicoq$(EXE)
$(MINICOQ): $(MINICOQCMO)
$(OCAMLC) $(INCLUDES) -o $@ -custom $(CMA) $(MINICOQCMO) $(OSDEPLIBS)
@@ -584,7 +578,7 @@ install-library:
$(MKDIR) $(FULLCOQLIB)/states
cp states/*.coq $(FULLCOQLIB)/states
$(MKDIR) $(FULLEMACSLIB)
- cp tools/coq.el tools/coq.elc $(FULLEMACSLIB)
+ cp tools/coq.el $(FULLEMACSLIB)
MANPAGES=tools/coq-tex.1 tools/coqdep.1 tools/gallina.1
@@ -707,7 +701,7 @@ clean::
$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
.v.vo:
- $(COQC) -q -$(BEST) -bindir bin $(COQINCLUDES) $<
+ $(COQC) -boot -$(BEST) $(COQINCLUDES) $<
.el.elc:
echo "(setq load-path (cons \".\" load-path))" > $*.compile
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 4f8c8f6d6..7482a45c9 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -23,7 +23,7 @@ val best : string (* byte/opt *)
val arch : string (* architecture *)
val osdeplibs : string (* OS dependant link options for ocamlc *)
-val defined : string list (* options for lib/ocamlpp *)
+(* val defined : string list (* options for lib/ocamlpp *) *)
val version : string (* version number of Coq *)
val versionsi : string (* version number of Coq\_SearchIsos *)
@@ -33,3 +33,4 @@ val compile_date : string (* compile date *)
val theories_dirs : string list
val contrib_dirs : string list
+val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
diff --git a/configure b/configure
index c9192ee98..3060aef34 100755
--- a/configure
+++ b/configure
@@ -183,16 +183,16 @@ case $emacslib_spec in
yes) EMACSLIB=$emacslib;;
esac
-case $emacs_spec in
- no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?"
- read EMACS
+# case $emacs_spec in
+# no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?"
+# read EMACS
- case $EMACS in
- "") EMACS=$emacs_def;;
- *) true;;
- esac;;
- yes) EMACS=$emacs;;
-esac
+# case $EMACS in
+# "") EMACS=$emacs_def;;
+# *) true;;
+# esac;;
+# yes) EMACS=$emacs;;
+# esac
# OS dependent libraries
@@ -383,59 +383,37 @@ rm -f $COQTOP/config/Makefile
case $ARCH in
win32)
- sed -e "s|LOCALINSTALLATION|$local|" \
- -e "s|COQTOPDIRECTORY|$COQTOP|" \
- -e "s|COQVERSION|$VERSION|" \
- -e "s|BINDIRDIRECTORY|`echo $BINDIR |sed -e 's|\\\|/|g'`|" \
- -e "s|COQLIBDIRECTORY|`echo $LIBDIR |sed -e 's|\\\|/|g'`|" \
- -e "s|MANDIRDIRECTORY|`echo $MANDIR |sed -e 's|\\\|/|g'`|" \
- -e "s|EMACSLIBDIRECTORY|`echo $EMACSLIB |sed -e 's|\\\|/|g'`|" \
- -e "s|EMACSCOMMAND|$EMACS|" \
- -e "s|ARCHITECTURE|$ARCH|" \
- -e "s|OSDEPENDANTLIBS|$OSDEPLIBS|" \
- -e "s|OSDEPENDANTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
- -e "s|STRLIBRARY|$WITH_STR|" \
- -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
- -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
- -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
- -e "s|CAMLP4TOOL|$camlp4o|" \
- -e "s|OSKIND|$OSTYPE|" \
- -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
- -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
- -e "s|BESTCOMPILER|$best_compiler|" \
- -e "s|EXECUTEEXTENSION|$EXE|" \
- -e "s|BYTECAMLC|$bytecamlc|" \
- -e "s|NATIVECAMLC|$nativecamlc|" \
- -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
- $COQTOP/config/Makefile.template > $COQTOP/config/Makefile;;
- *)
- sed -e "s|LOCALINSTALLATION|$local|" \
- -e "s|COQTOPDIRECTORY|$COQTOP|" \
- -e "s|COQVERSION|$VERSION|" \
- -e "s|BINDIRDIRECTORY|$BINDIR|" \
- -e "s|COQLIBDIRECTORY|$LIBDIR|" \
- -e "s|MANDIRDIRECTORY|$MANDIR|" \
- -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
- -e "s|EMACSCOMMAND|$EMACS|" \
- -e "s|ARCHITECTURE|$ARCH|" \
- -e "s|OSDEPENDANTLIBS|$OSDEPLIBS|" \
- -e "s|OSDEPENDANTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
- -e "s|STRLIBRARY|$WITH_STR|" \
- -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
- -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
- -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
- -e "s|CAMLP4TOOL|$camlp4o|" \
- -e "s|OSKIND|$OSTYPE|" \
- -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
- -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
- -e "s|BESTCOMPILER|$best_compiler|" \
- -e "s|EXECUTEEXTENSION|$EXE|" \
- -e "s|BYTECAMLC|$bytecamlc|" \
- -e "s|NATIVECAMLC|$nativecamlc|" \
- -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
- $COQTOP/config/Makefile.template > $COQTOP/config/Makefile;;
+ BINDIR=`echo $BINDIR |sed -e 's|\\\|/|g'`
+ LIBDIR=`echo $LIBDIR |sed -e 's|\\\|/|g'`
+ MANDIR=`echo $MANDIR |sed -e 's|\\\|/|g'`;;
esac
+sed -e "s|LOCALINSTALLATION|$local|" \
+ -e "s|COQTOPDIRECTORY|$COQTOP|" \
+ -e "s|COQVERSION|$VERSION|" \
+ -e "s|BINDIRDIRECTORY|$BINDIR|" \
+ -e "s|COQLIBDIRECTORY|$LIBDIR|" \
+ -e "s|MANDIRDIRECTORY|$MANDIR|" \
+ -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
+ -e "s|EMACSCOMMAND|$EMACS|" \
+ -e "s|ARCHITECTURE|$ARCH|" \
+ -e "s|OSDEPENDANTLIBS|$OSDEPLIBS|" \
+ -e "s|OSDEPENDANTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
+ -e "s|STRLIBRARY|$WITH_STR|" \
+ -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
+ -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
+ -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
+ -e "s|CAMLP4TOOL|$camlp4o|" \
+ -e "s|OSKIND|$OSTYPE|" \
+ -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
+ -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
+ -e "s|BESTCOMPILER|$best_compiler|" \
+ -e "s|EXECUTEEXTENSION|$EXE|" \
+ -e "s|BYTECAMLC|$bytecamlc|" \
+ -e "s|NATIVECAMLC|$nativecamlc|" \
+ -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
+ $COQTOP/config/Makefile.template > $COQTOP/config/Makefile
+
chmod a-w $COQTOP/config/Makefile
# Building the $COQTOP/dev/ocamldebug-v7 file
@@ -466,11 +444,12 @@ let camlp4lib = "$CAMLP4LIB"
let best = "$best_compiler"
let arch = "$ARCH"
let osdeplibs = "$OSDEPLIBS"
-let defined = [ "$OSTYPE" ]
+(* let defined = [ "$OSTYPE" ] *)
let version = "$VERSION"
let versionsi = "$VERSIONSI"
let date = "$DATE"
let compile_date = "$COMPILEDATE"
+let exec_extension = "$EXE"
END_OF_COQ_CONFIG
diff --git a/distrib/Makefile b/distrib/Makefile
index 88f870a47..0bb793b5b 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -1,6 +1,6 @@
# Building the different files of the coq distribution
-include config.distrib
+sinclude config.distrib
LOCALARCH=`uname -m`
ARCH=`uname -m | sed -e 's/i.86/i386/'`
SYSTEM=`uname -s`
@@ -41,6 +41,7 @@ noarguments:
@echo "make arch-rpm-ftp-install |repository supposed"
@echo "make arch-tar-gz-ftp-install |to be already"
@echo "make contrib-ftp-install |prepared"
+ @echo "make deb to build a debian package"
################## Main targets
@@ -259,3 +260,8 @@ contrib-ftp-install: prep-ftp-install
patch-ftp-install: prep-ftp-install
cp patch-${VERSION}-$(PREVIOUSVERSION).gz ${FTPDIR}/V${VERSION}/
chmod g+w ${FTPDIR}/V${VERSION}/patch-${VERSION}-$(PREVIOUSVERSION).gz
+
+deb:
+ rm -rf ../debian
+ cp -a debian ..
+ cd .. ; dpkg-buildpackage -rfakeroot -uc -us
diff --git a/lib/options.ml b/lib/options.ml
index 52babfdb2..b00d52373 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -10,6 +10,8 @@
open Util
+let boot = ref false
+
let batch_mode = ref false
let debug = ref false
diff --git a/lib/options.mli b/lib/options.mli
index 8d1d7e2fd..e70d38669 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -10,6 +10,8 @@
(* Global options of the system. *)
+val boot : bool ref
+
val batch_mode : bool ref
val debug : bool ref
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 0ef69ab08..022656720 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -127,6 +127,9 @@ let parse_args () =
keep := true ; parse (cfiles,args) rem
| ("-verbose" | "--verbose") :: rem ->
verbose := true ; parse (cfiles,args) rem
+ | "-boot" :: rem ->
+ bindir:= Filename.concat Coq_config.coqtop "bin";
+ parse (cfiles, "-boot"::args) rem
| "-bindir" :: d :: rem ->
bindir := d ; parse (cfiles,args) rem
| "-bindir" :: [] ->
@@ -182,7 +185,7 @@ let main () =
usage ()
end;
let coqtopname =
- if !image <> "" then !image else Filename.concat !bindir !binary
+ if !image <> "" then !image else Filename.concat !bindir (!binary ^ Coq_config.exec_extension)
in
List.iter (compile coqtopname args) cfiles
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 7b3fa1628..01dec915a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -70,22 +70,14 @@ let getenv_else s dft = try Sys.getenv s with Not_found -> dft
(* Initializes the LoadPath according to COQLIB and Coq_config *)
let init_load_path () =
- if Coq_config.local then begin
- (* local use (no installation) *)
- List.iter
- (fun s -> coq_add_path (Filename.concat Coq_config.coqtop s))
- ["states"; "dev"];
- coq_add_rec_path (Filename.concat Coq_config.coqtop "theories");
- coq_add_path (Filename.concat Coq_config.coqtop "tactics");
- coq_add_rec_path (Filename.concat Coq_config.coqtop "contrib")
- end else begin
- (* default load path; variable COQLIB overrides the default library *)
- let coqlib = getenv_else "COQLIB" Coq_config.coqlib in
- coq_add_path (Filename.concat coqlib "states");
- coq_add_rec_path (Filename.concat coqlib "theories");
- coq_add_path (Filename.concat coqlib "tactics");
- coq_add_rec_path (Filename.concat coqlib "contrib")
- end;
+ (* developper specific directories to open *)
+ let dev = if Coq_config.local then [ "dev" ] else [] in
+ let dirs = "states" :: dev @ [ "theories"; "tactics"; "contrib" ] in
+ let coqlib =
+ if Coq_config.local || !Options.boot then Coq_config.coqtop
+ (* variable COQLIB overrides the default library *)
+ else getenv_else "COQLIB" Coq_config.coqlib in
+ List.iter (fun s -> coq_add_rec_path (Filename.concat coqlib s)) dirs;
let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
add_ml_include camlp4;
Mltop.add_path "." [Nametab.default_root];
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0778b7735..9e9c3436a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -120,7 +120,8 @@ let parse_args () =
| "-full" :: rem -> warning "option -full deprecated\n"; parse rem
| "-batch" :: rem -> set_batch_mode (); parse rem
-
+ | "-boot" :: rem -> boot := true; no_load_rc (); set_batch_mode ();
+ parse rem
| "-outputstate" :: s :: rem -> set_outputstate s; parse rem
| "-outputstate" :: [] -> usage ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8dc848d3c..f9d5decd9 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -47,6 +47,7 @@ let print_usage_channel co command =
-init-file f set the rcfile to f
-user u use the rcfile of user u
-batch batch mode (exits just after arguments parsing)
+ -boot boot mode (implies -q and -batch)
-emacs tells Coq it is executed under Emacs
"
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 01:57:58 +0000