diff options
| -rw-r--r-- | Makefile.checker | 11 | ||||
| -rw-r--r-- | Makefile.dev | 2 | ||||
| -rw-r--r-- | Makefile.dune | 2 | ||||
| -rw-r--r-- | dev/checker.dbg | 7 | ||||
| -rw-r--r-- | dev/checker_db | 5 | ||||
| -rw-r--r-- | dev/checker_dune_db | 5 | ||||
| -rw-r--r-- | dev/checker_printers.dbg | 35 | ||||
| -rw-r--r-- | dev/checker_printers.ml | 69 | ||||
| -rw-r--r-- | dev/checker_printers.mli | 50 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 2 | ||||
| -rw-r--r-- | dev/dune | 11 | ||||
| -rwxr-xr-x | dev/dune-dbg.in | 14 |
12 files changed, 13 insertions, 200 deletions
diff --git a/Makefile.checker b/Makefile.checker index a0f0778d49..7440c767e6 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -59,8 +59,7 @@ checker/check.cmxa: checker/check.mllib $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) -CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) \ - $(filter dev/checker_%, $(MLFILES) $(MLIFILES)) +CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) $(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES)) $(SHOW)'OCAMLDEP checker/MLFILES checker/MLIFILES' @@ -82,14 +81,6 @@ checker/%.cmx: checker/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $< -dev/checker_%.cmo: dev/checker_%.ml - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $< - -dev/checker_%.cmi: dev/checker_%.mli - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $< - # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.dev b/Makefile.dev index 54710b6690..9659f602d7 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -17,7 +17,7 @@ .PHONY: devel printers -DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo +DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo devel: printers printers: $(CORECMA) $(DEBUGPRINTERS) diff --git a/Makefile.dune b/Makefile.dune index d201d1783a..11a31b174d 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -42,7 +42,7 @@ check: voboot COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc PLUGIN_FILES=$(wildcard plugins/*/*.mlpack) -PRINTER_FILES=dev/top_printers.cma dev/checker_printers.cma +PRINTER_FILES=dev/top_printers.cma QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxa) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe diff --git a/dev/checker.dbg b/dev/checker.dbg deleted file mode 100644 index b5b7f0e6d3..0000000000 --- a/dev/checker.dbg +++ /dev/null @@ -1,7 +0,0 @@ -load_printer threads.cma -load_printer str.cma -load_printer clib.cma -load_printer dynlink.cma -load_printer config.cma -load_printer lib.cma -load_printer check.cma diff --git a/dev/checker_db b/dev/checker_db deleted file mode 100644 index fcb6f679ed..0000000000 --- a/dev/checker_db +++ /dev/null @@ -1,5 +0,0 @@ -source checker.dbg - -load_printer checker_printers.cmo - -source checker_printers.dbg diff --git a/dev/checker_dune_db b/dev/checker_dune_db deleted file mode 100644 index cdb6a4b809..0000000000 --- a/dev/checker_dune_db +++ /dev/null @@ -1,5 +0,0 @@ -source checker_dune.dbg - -load_printer checker_printers.cma - -source checker_printers.dbg diff --git a/dev/checker_printers.dbg b/dev/checker_printers.dbg deleted file mode 100644 index 9ebbd74834..0000000000 --- a/dev/checker_printers.dbg +++ /dev/null @@ -1,35 +0,0 @@ -install_printer Checker_printers.pP - -install_printer Checker_printers.ppfuture - -install_printer Checker_printers.ppid -install_printer Checker_printers.pplab -install_printer Checker_printers.ppmbid -install_printer Checker_printers.ppdir -install_printer Checker_printers.ppmp -install_printer Checker_printers.ppcon -install_printer Checker_printers.ppproj -install_printer Checker_printers.ppkn -install_printer Checker_printers.ppmind -install_printer Checker_printers.ppind - -install_printer Checker_printers.ppbigint - -install_printer Checker_printers.ppintset -install_printer Checker_printers.ppidset - -install_printer Checker_printers.ppidmapgen - -install_printer Checker_printers.ppididmap - -install_printer Checker_printers.ppuni -install_printer Checker_printers.ppuni_level -install_printer Checker_printers.ppuniverse_set -install_printer Checker_printers.ppuniverse_instance -install_printer Checker_printers.ppauniverse_context -install_printer Checker_printers.ppuniverse_context -install_printer Checker_printers.ppconstraints -install_printer Checker_printers.ppuniverse_context_future -install_printer Checker_printers.ppuniverses - -install_printer Checker_printers.pploc diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml deleted file mode 100644 index 4f89bbd34e..0000000000 --- a/dev/checker_printers.ml +++ /dev/null @@ -1,69 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open Names -open Univ - -let pp x = Pp.pp_with Format.std_formatter x - -(** Future printer *) - -let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) - -(* name printers *) -let ppid id = pp (Id.print id) -let pplab l = pp (Label.print l) -let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) -let ppdir dir = pp (DirPath.print dir) -let ppmp mp = pp(str (ModPath.debug_to_string mp)) -let ppcon con = pp(Constant.debug_print con) -let ppproj con = pp(Constant.debug_print (Projection.constant con)) -let ppkn kn = pp(str (KerName.to_string kn)) -let ppmind kn = pp(MutInd.debug_print kn) -let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i) - -(* term printers *) -let ppbigint n = pp (str (Bigint.to_string n));; - -let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" -let ppintset l = pp (prset int (Int.Set.elements l)) -let ppidset l = pp (prset Id.print (Id.Set.elements l)) - -let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" - -let pridmap pr l = - let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in - prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []) -let ppidmap pr l = pp (pridmap pr l) - -let pridmapgen l = - let dom = Id.Set.elements (Id.Map.domain l) in - if dom = [] then str "[]" else - str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]" -let ppidmapgen l = pp (pridmapgen l) - -let prididmap = pridmap (fun _ -> Id.print) -let ppididmap = ppidmap (fun _ -> Id.print) - -let pP s = pp (hov 0 s) - -(* proof printers *) -let ppuni u = pp(Universe.pr u) -let ppuni_level u = pp (Level.pr u) - -let ppuniverse_context l = pp (pr_universe_context Level.pr l) -let ppconstraints c = pp (pr_constraints Level.pr c) -let ppuniverse_context_future c = - let ctx = Future.force c in - ppuniverse_context ctx - -let pploc x = let (l,r) = Loc.unloc x in - print_string"(";print_int l;print_string",";print_int r;print_string")" diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli deleted file mode 100644 index 8be9b87257..0000000000 --- a/dev/checker_printers.mli +++ /dev/null @@ -1,50 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Printers for the ocaml toplevel. *) - -val pp : Pp.t -> unit -val pP : Pp.t -> unit (* with surrounding box *) - -val ppfuture : 'a Future.computation -> unit - -val ppid : Names.Id.t -> unit -val pplab : Names.Label.t -> unit -val ppmbid : Names.MBId.t -> unit -val ppdir : Names.DirPath.t -> unit -val ppmp : Names.ModPath.t -> unit -val ppcon : Names.Constant.t -> unit -val ppproj : Names.Projection.t -> unit -val ppkn : Names.KerName.t -> unit -val ppmind : Names.MutInd.t -> unit -val ppind : Names.inductive -> unit - -val ppbigint : Bigint.bigint -> unit - -val ppintset : Int.Set.t -> unit -val ppidset : Names.Id.Set.t -> unit - -val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t -val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit - -val pridmapgen : 'a Names.Id.Map.t -> Pp.t -val ppidmapgen : 'a Names.Id.Map.t -> unit - -val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t -val ppididmap : Names.Id.t Names.Id.Map.t -> unit - -(* Universes *) -val ppuni : Univ.Universe.t -> unit -val ppuni_level : Univ.Level.t -> unit (* raw *) -val ppuniverse_context : Univ.UContext.t -> unit -val ppconstraints : Univ.Constraint.t -> unit -val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit - -val pploc : Loc.t -> unit diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0aeb30c4e8..c5ea88aaf6 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -81,7 +81,7 @@ or ``` dune exec dev/dune-dbg checker -(ocd) source checker_dune_db +(ocd) source dune_db ``` for the checker. Unfortunately, dependency handling here is not fully @@ -3,18 +3,9 @@ (public_name coq.top_printers) (synopsis "Coq's Debug Printers") (wrapped false) - (modules :standard \ checker_printers) + (modules :standard) (libraries coq.toplevel coq.plugins.ltac)) -(library - (name checker_printers) - (public_name coq.checker_printers) - (synopsis "Coq's Debug Printers [for the Checker]") - (wrapped false) - (flags :standard -open Checklib) - (modules checker_printers) - (libraries coq.checklib)) - (rule (targets dune-dbg) (deps dune-dbg.in diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 464e026400..3f3df23fe1 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -2,10 +2,12 @@ # Run in a proper install dune env. case $1 in -checker) - ocamldebug `ocamlfind query -recursive -i-format coq.checker_printers` -I +threads -I dev _build/default/checker/main.bc - ;; -*) - ocamldebug `ocamlfind query -recursive -i-format coq.top_printers` -I +threads -I dev _build/default/topbin/coqtop_byte_bin.bc - ;; + checker) + exe=_build/default/checker/main.bc + ;; + *) + exe=_build/default/topbin/coqtop_byte_bin.bc + ;; esac + +ocamldebug $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe |