aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in8
-rw-r--r--tools/coq_dune.ml2
-rw-r--r--tools/coq_makefile.ml26
-rw-r--r--tools/coq_tex.ml3
-rw-r--r--tools/coqdep.ml2
-rw-r--r--tools/coqdoc/cdglobals.ml5
-rw-r--r--tools/coqdoc/cpretty.mll1
-rw-r--r--tools/coqdoc/output.ml2
8 files changed, 25 insertions, 24 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index f8f10b34ae..bd9d8c9221 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -187,7 +187,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
COQMAKEFILE_VERSION:=@COQ_VERSION@
-COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
+COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
@@ -216,9 +216,9 @@ endif
concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
-COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib)
-COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib)
-COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop)
+COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib)
+COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib)
+COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
# Files #######################################################################
#
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 68371edcb1..62a871aa0e 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -186,7 +186,7 @@ let pp_vo_dep dir fmt vo =
(* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *)
let libflag = "-coqlib %{project_root}" in
(* The final build rule *)
- let action = sprintf "(chdir %%{project_root} (run coqc -boot %s %s %s %s))" libflag eflag cflag source in
+ let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in
let all_targets = gen_coqc_targets vo in
pp_rule fmt all_targets deps action
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 5526970d3f..68281d6481 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -123,9 +123,10 @@ let read_whole_file s =
let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s
let generate_makefile oc conf_file local_file args project =
+ let coqlib = Envars.coqlib () in
let makefile_template =
- let template = "/tools/CoqMakefile.in" in
- Envars.coqlib () ^ template in
+ let template = Filename.concat "tools" "CoqMakefile.in" in
+ Filename.concat coqlib template in
let s = read_whole_file makefile_template in
let s = List.fold_left
(* We use global_substitute to avoid running into backslash issues due to \1 etc. *)
@@ -260,7 +261,7 @@ let generate_conf_doc oc { defs; q_includes; r_includes } =
eprintf "Warning: in %s\n" destination;
destination
end else "$(INSTALLDEFAULTROOT)"
- else String.concat "/" gcd in
+ else String.concat Filename.dir_sep gcd in
Printf.fprintf oc "COQMF_INSTALLCOQDOCROOT = %s\n" (quote root)
let generate_conf_defs oc { defs; extra_args } =
@@ -343,15 +344,13 @@ let chop_prefix p f =
let len_f = String.length f in
String.sub f len_p (len_f - len_p)
-let clean_path p =
- Str.global_replace (Str.regexp_string "//") "/" p
-
let destination_of { ml_includes; q_includes; r_includes; } file =
let file_dir = CUnix.canonical_path_name (Filename.dirname file) in
let includes = q_includes @ r_includes in
let mk_destination logic canonical_path =
- clean_path (physical_dir_of_logical_dir logic ^ "/" ^
- chop_prefix canonical_path file_dir ^ "/") in
+ Filename.concat
+ (physical_dir_of_logical_dir logic)
+ (chop_prefix canonical_path file_dir) in
let candidates =
CList.map_filter (fun {thing={ canonical_path }, logic} ->
if is_prefix canonical_path file_dir then
@@ -368,8 +367,9 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
with
| [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} ->
let destination =
- clean_path (physical_dir_of_logical_dir logic ^ "/" ^
- chop_prefix p file_dir ^ "/") in
+ Filename.concat
+ (physical_dir_of_logical_dir logic)
+ (chop_prefix p file_dir) in
Printf.printf "%s" (quote destination)
| _ -> () (* skip *)
| exception Not_found -> () (* skip *)
@@ -424,15 +424,15 @@ let _ =
end;
let project = ensure_root_dir project in
-
+
if project.install_kind <> (Some CoqProject_file.NoInstall) then begin
warn_install_at_root_directory project;
end;
check_overlapping_include project;
- Envars.set_coqlib ~boot:false ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1);
-
+ Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1);
+
let ocm = Option.cata open_out stdout project.makefile in
generate_makefile ocm conf_file local_file (prog :: args) project;
close_out ocm;
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 0ffa5bd7e4..c6d3551561 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -259,8 +259,6 @@ let parse_cl () =
" Coq parts are written between 2 horizontal lines";
"-small", Arg.Set small,
" Coq parts are written in small font";
- "-boot", Arg.Set boot,
- " Launch coqtop with the -boot option"
]
(fun s -> files := s :: !files)
"coq-tex [options] file ..."
@@ -279,7 +277,6 @@ let find_coqtop () =
let _ =
parse_cl ();
if !image = "" then image := Filename.quote (find_coqtop ());
- if !boot then image := !image ^ " -boot";
if Sys.command (!image ^ " -batch -silent") <> 0 then begin
Printf.printf "Error: ";
let _ = Sys.command (!image ^ " -batch") in
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 5f8cc99ed1..66f1f257b8 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -531,7 +531,7 @@ let coqdep () =
add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
end else begin
(* option_boot is actually always false in this branch *)
- Envars.set_coqlib ~boot:!option_boot ~fail:(fun msg -> raise (CoqlibError msg));
+ Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
let coqlib = Envars.coqlib () in
add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 0d3fb77551..5dd6cc6c83 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -79,14 +79,17 @@ let use_suffix prefix suffix =
(** A weaker analog of the function in Envars *)
+let getenv_else s dft = try Sys.getenv s with Not_found -> dft ()
+
let guess_coqlib () =
+ getenv_else "COQLIB" (fun () ->
let file = "theories/Init/Prelude.vo" in
let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
let prefix = Filename.dirname coqbin in
let coqlib = use_suffix prefix Coq_config.coqlibsuffix in
if Sys.file_exists (coqlib / file) then coqlib else
if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file)
- then Coq_config.coqlib else prefix
+ then Coq_config.coqlib else prefix)
let header_trailer = ref true
let header_file = ref ""
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 1be440a750..230c5524b7 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -409,6 +409,7 @@ let set_kw =
let gallina_kw_to_hide =
"Implicit" space+ "Arguments"
| ("Local" space+)? "Ltac"
+ | "From"
| "Require"
| "Import"
| "Export"
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 606d954672..b703af934d 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -32,7 +32,7 @@ let is_keyword =
build_table
[ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
"CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
- "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar";
+ "Export"; "Fact"; "Fix"; "Fixpoint"; "From"; "Function"; "Generalizable"; "Global"; "Grammar";
"Guarded"; "Goal"; "Hint"; "Debug"; "On";
"Hypothesis"; "Hypotheses";
"Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite";
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 20:44:48 +0000