aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend.camlp414
-rw-r--r--Makefile77
-rw-r--r--parsing/extend.ml44
-rw-r--r--parsing/g_basevernac.ml42
-rw-r--r--parsing/g_cases.ml42
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_minicoq.ml42
-rw-r--r--parsing/g_prim.ml42
-rw-r--r--parsing/g_tactic.ml42
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/pcoq.ml42
-rw-r--r--scripts/.cvsignore1
-rw-r--r--scripts/coqc.ml (renamed from scripts/coqc.ml4)2
-rw-r--r--tactics/tauto.ml45
14 files changed, 63 insertions, 56 deletions
diff --git a/.depend.camlp4 b/.depend.camlp4
index 2fb1b6be6..f94110020 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -4,8 +4,6 @@ tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
proofs/tacmach.cmx tactics/tacticals.cmx
-scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi
-scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx
parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi
parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmx
parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi
@@ -46,3 +44,15 @@ toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \
lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \
toplevel/vernacinterp.cmx toplevel/mltop.cmi
+tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
+parsing/q_coqast.ml:
+parsing/g_prim.ml:
+parsing/pcoq.ml:
+parsing/g_basevernac.ml: parsing/grammar.cma
+parsing/g_minicoq.ml: parsing/grammar.cma
+parsing/g_vernac.ml: parsing/grammar.cma
+parsing/g_cases.ml: parsing/grammar.cma
+parsing/g_constr.ml: parsing/grammar.cma
+parsing/g_tactic.ml: parsing/grammar.cma
+parsing/extend.ml: parsing/grammar.cma
+toplevel/mltop.ml:
diff --git a/Makefile b/Makefile
index 854e73725..8fc23d483 100644
--- a/Makefile
+++ b/Makefile
@@ -39,10 +39,10 @@ OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
OCAMLDEP=ocamldep
DEPFLAGS=$(LOCALINCLUDES)
-CAMLP4ARGS=$(INCLUDES) pa_extend.cmo
OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
-CAMLP4IFDEF=pa_ifdef.cmo -D$(OSTYPE)
+CAMLP4O=camlp4o -I . pa_extend.cmo q_MLast.cmo
+CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p'
COQINCLUDES=-I contrib/omega -I contrib/ring -I contrib/xml \
-I theories/Init -I theories/Logic -I theories/Arith \
@@ -122,7 +122,6 @@ HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \
SPECTAC=tactics/tauto.ml4
USERTAC = $(SPECTAC)
ML4FILES += $(USERTAC)
-USERTACML=$(USERTAC:.ml4=.ml)
USERTACCMO=$(USERTAC:.ml4=.cmo)
USERTACCMX=$(USERTAC:.ml4=.cmx)
@@ -152,7 +151,7 @@ world: $(COQBINARIES) states theories contrib tools
coqtop.opt: $(COQMKTOP) $(CMX) $(USERTACCMX)
$(COQMKTOP) -opt $(OPTFLAGS) -o coqtop.opt
-# $(STRIP) ./coqtop.opt
+ $(STRIP) ./coqtop.opt
coqtop.byte: $(COQMKTOP) $(CMO) $(USERTACCMO)
$(COQMKTOP) -top $(BYTEFLAGS) -o coqtop.byte
@@ -187,9 +186,6 @@ $(COQC): $(COQCCMO) coqtop.byte coqtop.$(BEST)
$(OCAMLC) $(BYTEFLAGS) -o $(COQC) -custom unix.cma $(COQCCMO) \
$(OSDEPLIBS)
-scripts/coqc.ml scripts/coqc.cmo scripts/coqc.cmx: CAMLP4ARGS=$(CAMLP4IFDEF)
-ML4FILES += scripts/coqc.ml4
-
archclean::
rm -f scripts/coqc scripts/coqmktop
@@ -222,8 +218,7 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \
theories/Init/Logic_Type.vo theories/Init/Wf.vo \
theories/Init/Logic_TypeSyntax.vo
-theories/Init/%.vo: $(COQC)
-theories/Init/%.vo: theories/Init/%.v states/barestate.coq
+theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC)
$(COQC) -q -I theories/Init -is states/barestate.coq $<
init: $(INITVO)
@@ -231,8 +226,7 @@ init: $(INITVO)
TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo \
tactics/EAuto.vo tactics/Refine.vo
-tactics/%.vo: $(COQC)
-tactics/%.vo: tactics/%.v states/barestate.coq
+tactics/%.vo: tactics/%.v states/barestate.coq $(COQC)
$(COQC) -q -I tactics -is states/barestate.coq $<
states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO) $(BESTCOQTOP)
@@ -346,20 +340,6 @@ archclean::
rm -f contrib/*/*.cmx contrib/*/*.[so]
###########################################################################
-# ML user tactics
-# (intended to be rather generic)
-###########################################################################
-
-CAMLP4GRAMMAR = -I parsing pa_extend.cmo grammar.cma
-
-COQCMO = names.cmo ast.cmo g_tactic.cmo g_constr.cmo
-
-$(USERTACML): CAMLP4ARGS=$(CAMLP4GRAMMAR) -I kernel $(COQCMO)
-$(USERTACCMO): CAMLP4ARGS=$(CAMLP4GRAMMAR) -I kernel $(COQCMO)
-$(USERTACCMX): CAMLP4ARGS=$(CAMLP4GRAMMAR) -I kernel $(COQCMO)
-
-
-###########################################################################
# tools
###########################################################################
@@ -405,7 +385,15 @@ minicoq: $(MINICOQCMO)
# Installation
###########################################################################
-install: install-binaries install-library install-manpages
+install: install-$(BEST) install-binaries install-library install-manpages
+
+install-byte:
+ cp $(COQMKTOP) $(COQC) coqtop.byte $(BINDIR)
+ cd $(BINDIR); ln -s coqtop.byte coqtop
+
+install-opt:
+ cp $(COQMKTOP) $(COQC) coqtop.byte coqtop.opt $(BINDIR)
+ cd $(BINDIR); ln -s coqtop.opt coqtop
install-binaries:
cp tools/coqdep tools/gallina tools/coq_makefile tools/coq-tex \
@@ -481,17 +469,7 @@ beforedepend:: parsing/lexer.ml
# grammar modules with camlp4
-QCOQAST=parsing/q_coqast.ml4
-ML4FILES += $(QCOQAST)
-$(QCOQAST:.ml4=.ml): CAMLP4ARGS=q_MLast.cmo
-$(QCOQAST:.ml4=.cmo): CAMLP4ARGS=q_MLast.cmo
-$(QCOQAST:.ml4=.cmx): CAMLP4ARGS=q_MLast.cmo
-
-GPRIM=parsing/g_prim.ml4 parsing/pcoq.ml4
-ML4FILES += $(GPRIM)
-$(GPRIM:.ml4=.ml): CAMLP4ARGS=pa_extend.cmo
-$(GPRIM:.ml4=.cmo): CAMLP4ARGS=pa_extend.cmo
-$(GPRIM:.ml4=.cmx): CAMLP4ARGS=pa_extend.cmo
+ML4FILES += parsing/q_coqast.ml4 parsing/g_prim.ml4 parsing/pcoq.ml4
GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/dyn.cmo \
lib/hashcons.cmo parsing/coqast.cmo parsing/lexer.cmo \
@@ -503,14 +481,9 @@ parsing/grammar.cma: $(GRAMMARCMO)
clean::
rm -f parsing/grammar.cma
-PARSINGML4=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \
+ML4FILES +=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \
parsing/g_vernac.ml4 parsing/g_cases.ml4 \
parsing/g_constr.ml4 parsing/g_tactic.ml4 parsing/extend.ml4
-ML4FILES += $(PARSINGML4)
-$(PARSINGML4:.ml4=.ml): parsing/grammar.cma
-$(PARSINGML4:.ml4=.cmo) $(PARSINGML4:.ml4=.cmx): parsing/grammar.cma
-$(PARSINGML4:.ml4=.ml): CAMLP4ARGS=$(CAMLP4GRAMMAR)
-$(PARSINGML4:.ml4=.cmo) $(PARSINGML4:.ml4=.cmx): CAMLP4ARGS=$(CAMLP4GRAMMAR)
beforedepend:: $(GRAMMARCMO)
@@ -518,12 +491,13 @@ beforedepend:: parsing/pcoq.ml parsing/extend.ml
# toplevel/mltop.ml4 (ifdef Byte)
-toplevel/mltop.ml: CAMLP4ARGS=$(CAMLP4IFDEF)
+toplevel/mltop.ml: toplevel/mltop.ml4
+ $(CAMLP4O) pr_o.cmo pa_ifdef.cmo -DByte -impl $< > $@ || rm -f $@
toplevel/mltop.cmo: toplevel/mltop.ml4
- $(OCAMLC) $(BYTEFLAGS) -pp "camlp4o $(CAMLP4IFDEF) -DByte -impl" \
+ $(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) pa_ifdef.cmo -DByte -impl" \
-c -impl $<
toplevel/mltop.cmx: toplevel/mltop.ml4
- $(OCAMLOPT) $(OPTFLAGS) -pp "camlp4o $(CAMLP4IFDEF) -impl" -c -impl $<
+ $(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) pa_ifdef.cmo -impl" -c -impl $<
ML4FILES += toplevel/mltop.ml4
###########################################################################
@@ -545,13 +519,13 @@ ML4FILES += toplevel/mltop.ml4
ocamllex $<
.ml4.cmo:
- $(OCAMLC) $(BYTEFLAGS) -pp "camlp4o $(CAMLP4ARGS) -impl" -c -impl $<
+ $(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
.ml4.cmx:
- $(OCAMLOPT) $(OPTFLAGS) -pp "camlp4o $(CAMLP4ARGS) -impl" -c -impl $<
+ $(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
.ml4.ml:
- camlp4o pr_o.cmo $(CAMLP4ARGS) -impl $< > $@ || rm -f $@
+ $(CAMLP4O) pr_o.cmo `$(CAMLP4DEPS) $<` -impl $< > $@ || rm -f $@
.v.vo:
$(COQC) -q -$(BEST) $(COQINCLUDES) $<
@@ -615,6 +589,11 @@ dependcoq: beforedepend
ML4FILESML = $(ML4FILES:.ml4=.ml)
dependcamlp4: beforedepend $(ML4FILESML)
ocamldep $(DEPFLAGS) $(ML4FILESML) > .depend.camlp4
+ for f in $(ML4FILES); do \
+ echo -n `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4; \
+ echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4; \
+ done
+ rm -f toplevel/mltop.ml
clean::
rm -f $(ML4FILESML)
diff --git a/parsing/extend.ml4 b/parsing/extend.ml4
index 1e2a00cce..aabd069bb 100644
--- a/parsing/extend.ml4
+++ b/parsing/extend.ml4
@@ -1,5 +1,7 @@
-(* $Id$ *)
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(*i $Id$ i*)
open Util
open Gramext
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 9fa032398..e8b40ccea 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -1,4 +1,6 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
(* $Id$ *)
open Coqast
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 5067b2aac..5418339f7 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -1,4 +1,6 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
(* $Id$ *)
open Pcoq
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index fac13a4e0..c7ab5fb85 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -1,4 +1,6 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
(* $Id$ *)
open Pcoq
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index d981109d5..e9f47b085 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -1,4 +1,6 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
(* $Id$ *)
open Pp
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 35d329177..30897a359 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
open Coqast
open Pcoq
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 311ca3371..b9c4b6a3e 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -1,4 +1,6 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
(* $Id$ *)
open Pp
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c4bc8fe13..f10a81d27 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1,4 +1,6 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
(* $Id$ *)
open Pcoq
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index a9338ff2b..2de8d52dd 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
open Pp
open Util
diff --git a/scripts/.cvsignore b/scripts/.cvsignore
index ee865a568..b95eb1ba9 100644
--- a/scripts/.cvsignore
+++ b/scripts/.cvsignore
@@ -1,4 +1,3 @@
coqmktop
tolink.ml
coqc
-coqc.ml
diff --git a/scripts/coqc.ml4 b/scripts/coqc.ml
index 5500903a9..baf86982b 100644
--- a/scripts/coqc.ml4
+++ b/scripts/coqc.ml
@@ -68,7 +68,7 @@ let compile command args file =
command :: "-batch" :: "-silent" :: args
@ ["-load-vernac-source"; tmpfile] in
let devnull =
- ifdef Unix then
+ if Sys.os_type = "Unix" then
Unix.openfile "/dev/null" [] 0o777
else
Unix.stdin
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index ec47a4756..57f95409f 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -1,3 +1,8 @@
+
+(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo" i*)
+
+(*i $Id$ i*)
+
open Ast
open Coqast
open Hipattern
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-01 13:48:39 +0000