aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/README.emacs31
-rwxr-xr-xtools/check-translate23
-rw-r--r--tools/coq-sl.sty37
-rw-r--r--tools/coq_dune.ml45
-rw-r--r--tools/coqc.ml8
-rw-r--r--tools/coqdep.ml2
-rw-r--r--tools/coqdep_common.ml6
-rw-r--r--tools/coqdep_lexer.mll9
-rw-r--r--tools/coqdoc/alpha.ml10
-rw-r--r--tools/coqdoc/dune8
-rw-r--r--tools/coqdoc/index.ml6
-rw-r--r--tools/coqdoc/output.ml11
-rw-r--r--tools/dune28
-rw-r--r--tools/mkwinapp.ml92
-rw-r--r--tools/ocamllibdep.mll9
15 files changed, 51 insertions, 274 deletions
diff --git a/tools/README.emacs b/tools/README.emacs
deleted file mode 100644
index 4d8e3697a0..0000000000
--- a/tools/README.emacs
+++ /dev/null
@@ -1,31 +0,0 @@
-
-DESCRIPTION:
-
-An emacs mode to help editing Coq vernacular files.
-
-AUTHOR:
-
-Jean-Christophe Filliatre (jcfillia@lri.fr),
- from the Caml mode of Xavier Leroy.
-
-CONTENTS:
-
- gallina.el A major mode for editing Coq files in Gnu Emacs
-
-USAGE:
-
-Add the following lines to your .emacs file:
-
-(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-(autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
-
-The Coq major mode is triggered by visiting a file with extension .v,
-or manually by M-x coq-mode. It gives you the correct syntax table for
-the Coq language, and also a rudimentary indentation facility:
-
-- pressing TAB at the beginning of a line indents the line like the line above
-
-- extra TABs increase the indentation level (by 2 spaces by default)
-
-- M-TAB decreases the indentation level.
-
diff --git a/tools/check-translate b/tools/check-translate
deleted file mode 100755
index acb6f45903..0000000000
--- a/tools/check-translate
+++ /dev/null
@@ -1,23 +0,0 @@
-#!/bin/sh
-
-echo -------------- Producing translated files ---------------------
-rm */*/*.v8 >& /dev/null
-make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; }
-if [ -e translated ]; then rm -r translated; fi
-if [ -e successful-translation ]; then rm -r successful-translation; fi
-if [ -e failed-translation ]; then rm -r failed-translation; fi
-mv theories translated
-mkdir theories
-echo -------------------- Upgrading files --------------------------
-cd translated
-for i in */*.v
-do
- mkdir ../theories/`dirname $i` >& /dev/null
- mv "$i"8 ../theories/$i
-done
-cd ..
-echo --------------- Recompiling translated files ------------------
-make theories || { echo ---- Failed to recompile; mv theories failed-translation; mv translated theories; exit 1; }
-echo ----------------- Recompilation successful --------------------
-if [ -e successful-translation ]; then rm -r successful-translation; fi
-mv theories successful-translation; mv translated theories
diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty
deleted file mode 100644
index 9f6e5480c9..0000000000
--- a/tools/coq-sl.sty
+++ /dev/null
@@ -1,37 +0,0 @@
-% COQ style option, for use with the coq-latex filter.
-
-\typeout{Document Style option `coq-sl' <7 Apr 92>.}
-
-\ifcase\@ptsize
- \font\sltt = cmsltt10
-\or \font\sltt = cmsltt10 \@halfmag
-\or \font\sltt = cmsltt10 \@magscale1
-\fi
-
-{\catcode`\^^M=\active %
- \gdef\@coqinputline#1^^M{\tt Coq < #1\par} %
- \gdef\@coqoutputline#1^^M{\sltt#1\par} } %
-\def\@coqblankline{\medskip}
-\chardef\@coqbackslash="5C
-
-\def\coq{
- \bgroup
- \flushleft
- \parindent 0pt
- \parskip 0pt
- \let\do\@makeother\dospecials
- \catcode`\^^M=\active
- \catcode`\\=0
- \catcode`\ \active
- \frenchspacing
- \@vobeyspaces
- \let\?\@coqinputline
- \let\:\@coqoutputline
- \let\;\@coqblankline
- \let\\\@coqbackslash
-}
-
-\def\endcoq{
- \endflushleft
- \egroup\noindent
-}
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index ab60920fbc..ff6cefdf24 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -92,41 +92,6 @@ module Aux = struct
| None -> DirMap.remove key map
| Some x -> DirMap.add key x map
- (* Available in OCaml >= 4.04 *)
- let split_on_char sep s =
- let open String in
- let r = ref [] in
- let j = ref (length s) in
- for i = length s - 1 downto 0 do
- if unsafe_get s i = sep then begin
- r := sub s (i + 1) (!j - i - 1) :: !r;
- j := i
- end
- done;
- sub s 0 !j :: !r
-
- (* Available in OCaml >= 4.04 *)
- let is_dir_sep = match Sys.os_type with
- | "Win32" -> fun s i -> s.[i] = '\\'
- | _ -> fun s i -> s.[i] = '/'
-
- let extension_len name =
- let rec check i0 i =
- if i < 0 || is_dir_sep name i then 0
- else if name.[i] = '.' then check i0 (i - 1)
- else String.length name - i0
- in
- let rec search_dot i =
- if i < 0 || is_dir_sep name i then 0
- else if name.[i] = '.' then check i (i - 1)
- else search_dot (i - 1)
- in
- search_dot (String.length name - 1)
-
- let remove_extension name =
- let l = extension_len name in
- if l = 0 then name else String.sub name 0 (String.length name - l)
-
end
let add_map_list key elem map =
@@ -205,18 +170,18 @@ let pp_vo_dep dir fmt vo =
(* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *)
let deps = List.map (fun s -> sdir ^ s) (edep @ vo.deps) in
(* The source file is also corrected as we will call coqtop from the top dir *)
- let source = String.concat "/" dir ^ "/" ^ Legacy.(remove_extension vo.target) ^ ".v" in
+ let source = String.concat "/" dir ^ "/" ^ Filename.(remove_extension vo.target) ^ ".v" in
(* The final build rule *)
let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in
pp_rule fmt [vo.target] deps action
let pp_ml4_dep _dir fmt ml =
- let target = Legacy.(remove_extension ml) ^ ".ml" in
+ let target = Filename.(remove_extension ml) ^ ".ml" in
let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in
pp_rule fmt [target] [ml] ml4_rule
let pp_mlg_dep _dir fmt ml =
- let target = Legacy.(remove_extension ml) ^ ".ml" in
+ let target = Filename.(remove_extension ml) ^ ".ml" in
let ml4_rule = "(run coqpp %{pp-file})" in
pp_rule fmt [target] [ml] ml4_rule
@@ -229,7 +194,7 @@ let out_install fmt dir ff =
let itarget = String.concat "/" dir in
let ff = pmap (function | VO vo -> Some vo.target | _ -> None) ff in
let pp_ispec fmt tg = fprintf fmt "(%s as %s)" tg (itarget^"/"^tg) in
- fprintf fmt "(install@\n @[(section lib)@\n(files @[%a@])@])@\n"
+ fprintf fmt "(install@\n @[(section lib)@\n(package coq)@\n(files @[%a@])@])@\n"
(pp_list pp_ispec sep) ff
(* For each directory, we must record two things, the build rules and
@@ -274,7 +239,7 @@ let parse_coqdep_line l =
begin match targets with
| [target] ->
let dir, target = Filename.(dirname target, basename target) in
- Some (Legacy.split_on_char '/' dir, VO { target; deps; })
+ Some (String.split_on_char '/' dir, VO { target; deps; })
(* Otherwise a vio file, we ignore *)
| _ -> None
end
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 90d8e67c1e..2cbf05bd8b 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -24,7 +24,7 @@
let environment = Unix.environment ()
-let binary = ref "coqtop"
+let use_bytecode = ref false
let image = ref ""
let verbose = ref false
@@ -69,8 +69,8 @@ let parse_args () =
verbose := true ; parse (cfiles,args) rem
| "-image" :: f :: rem -> image := f; parse (cfiles,args) rem
| "-image" :: [] -> usage ()
- | "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem
- | "-opt" :: rem -> binary := "coqtop"; parse (cfiles,args) rem
+ | "-byte" :: rem -> use_bytecode := true; parse (cfiles,args) rem
+ | "-opt" :: rem -> use_bytecode := false; parse (cfiles,args) rem
(* Informative options *)
@@ -155,7 +155,7 @@ let main () =
end;
let coqtopname =
if !image <> "" then !image
- else Filename.concat Envars.coqbin (!binary ^ Coq_config.exec_extension)
+ else System.get_toplevel_path ~byte:!use_bytecode "coqtop"
in
(* List.iter (compile coqtopname args) cfiles*)
Unix.handle_unix_error (compile coqtopname args) cfiles
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 7db0b28908..ba88069be9 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -496,7 +496,7 @@ let rec parse = function
| "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
| "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse ll
| "-exclude-dir" :: [] -> usage ()
- | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
+ | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll
| "-coqlib" :: [] -> usage ()
| "-suffix" :: s :: ll -> suffixe := s ; parse ll
| "-suffix" :: [] -> usage ()
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 23b8bc112e..6a913ea894 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -41,10 +41,6 @@ let norec_dirs = ref StrSet.empty
let suffixe = ref ".vo"
-[@@@ocaml.warning "-3"] (* String.capitalize_ascii since 4.03.0 GPR#124 *)
-let capitalize = String.capitalize
-[@@@ocaml.warning "+3"]
-
type dir = string option
(** [get_extension f l] checks whether [f] has one of the extensions
@@ -473,7 +469,7 @@ let mL_dependencies () =
printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
- let efullname_capital = capitalize (Filename.basename efullname) in
+ let efullname_capital = String.capitalize_ascii (Filename.basename efullname) in
List.iter (fun dep ->
printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital)
dep;
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index ade5e5be6f..5533ab106d 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -52,9 +52,6 @@
let s = Lexing.lexeme lexbuf in
check_valid lexbuf (String.sub s 1 (String.length s - 1))
- [@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *)
- let uncapitalize = String.uncapitalize
- [@@@ocaml.warning "+3"]
}
let space = [' ' '\t' '\n' '\r']
@@ -159,7 +156,7 @@ and caml_action = parse
| space +
{ caml_action lexbuf }
| "open" space* (caml_up_ident as id)
- { Use_module (uncapitalize id) }
+ { Use_module (String.uncapitalize_ascii id) }
| "module" space+ caml_up_ident
{ caml_action lexbuf }
| caml_low_ident { caml_action lexbuf }
@@ -326,12 +323,12 @@ and modules mllist = parse
and qual_id ml_module_name = parse
| '.' [^ '.' '(' '[']
- { Use_module (uncapitalize ml_module_name) }
+ { Use_module (String.uncapitalize_ascii ml_module_name) }
| eof { raise Fin_fichier }
| _ { caml_action lexbuf }
and mllib_list = parse
- | caml_up_ident { let s = uncapitalize (Lexing.lexeme lexbuf)
+ | caml_up_ident { let s = String.uncapitalize_ascii (Lexing.lexeme lexbuf)
in s :: mllib_list lexbuf }
| "*predef*" { mllib_list lexbuf }
| space+ { mllib_list lexbuf }
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index 269c1a1d50..36ce405fe6 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -10,11 +10,7 @@
open Cdglobals
-[@@@ocaml.warning "-3"] (* Char.uppercase_ascii since 4.03.0 GPR#124 *)
-let uppercase = Char.uppercase
-[@@@ocaml.warning "+3"]
-
-let norm_char_latin1 c = match uppercase c with
+let norm_char_latin1 c = match Char.uppercase_ascii c with
| '\192'..'\198' -> 'A'
| '\199' -> 'C'
| '\200'..'\203' -> 'E'
@@ -25,12 +21,12 @@ let norm_char_latin1 c = match uppercase c with
| '\221' -> 'Y'
| c -> c
-let norm_char_utf8 c = uppercase c
+let norm_char_utf8 c = Char.uppercase_ascii c
let norm_char c =
if !utf8 then norm_char_utf8 c else
if !latin1 then norm_char_latin1 c else
- uppercase c
+ Char.uppercase_ascii c
let norm_string = String.map (fun s -> norm_char s)
diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune
index 8e05c7d97e..9c0a6ccffe 100644
--- a/tools/coqdoc/dune
+++ b/tools/coqdoc/dune
@@ -1,6 +1,14 @@
+(install
+ (section lib)
+ (package coq)
+ (files
+ (coqdoc.css as tools/coqdoc/coqdoc.css)
+ (coqdoc.sty as tools/coqdoc/coqdoc.sty)))
+
(executable
(name main)
(public_name coqdoc)
+ (package coq)
(libraries str coq.config))
(ocamllex cpretty)
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 724d3838b0..8d395b418f 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -157,14 +157,10 @@ let sort_entries el =
let display_letter c = if c = '*' then "other" else String.make 1 c
-[@@@ocaml.warning "-3"] (* String.lowercase_ascii since 4.03.0 GPR#124 *)
-let lowercase = String.lowercase
-[@@@ocaml.warning "+3"]
-
let type_name = function
| Library ->
let ln = !lib_name in
- if ln <> "" then lowercase ln else "library"
+ if ln <> "" then String.lowercase_ascii ln else "library"
| Module -> "module"
| Definition -> "definition"
| Inductive -> "inductive"
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 05bc6aea9b..8ec8927abd 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -21,11 +21,6 @@ let printf s = Printf.fprintf !out_channel s
let sprintf = Printf.sprintf
-[@@@ocaml.warning "-3"] (* String.{capitalize,lowercase}_ascii since 4.03.0 GPR#124 *)
-let capitalize = String.capitalize
-let lowercase = String.lowercase
-[@@@ocaml.warning "+3"]
-
(*s Coq keywords *)
let build_table l =
@@ -848,7 +843,7 @@ module Html = struct
if t = Library then
let ln = !lib_name in
if ln <> "" then
- "[" ^ lowercase ln ^ "]", m ^ ".html", t
+ "[" ^ String.lowercase_ascii ln ^ "]", m ^ ".html", t
else
"[library]", m ^ ".html", t
else
@@ -866,7 +861,7 @@ module Html = struct
(* Impression de la table d'index *)
let print_index_table_item i =
- printf "<tr>\n<td>%s Index</td>\n" (capitalize i.idx_name);
+ printf "<tr>\n<td>%s Index</td>\n" (String.capitalize_ascii i.idx_name);
List.iter
(fun (c,l) ->
if l <> [] then
@@ -914,7 +909,7 @@ module Html = struct
let print_table () = print_index_table all_index in
let print_one_index i =
if i.idx_size > 0 then begin
- printf "<hr/>\n<h1>%s Index</h1>\n" (capitalize i.idx_name);
+ printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize_ascii i.idx_name);
all_letters i
end
in
diff --git a/tools/dune b/tools/dune
index 05a620fb07..3358d1a4e2 100644
--- a/tools/dune
+++ b/tools/dune
@@ -1,22 +1,31 @@
-(executable
- (name coqc)
- (public_name coqc)
- (modules coqc)
- (libraries coq.toplevel))
+(install
+ (section lib)
+ (package coq)
+ (files
+ (CoqMakefile.in as tools/CoqMakefile.in)
+ (TimeFileMaker.py as tools/TimeFileMaker.py)
+ (make-one-time-file.py as tools/make-one-time-file.py)
+ (make-both-time-files.py as tools/make-both-time-files.py)
+ (make-both-single-timing-files.py as tools/make-both-single-timing-files.py)))
(executable
(name coq_makefile)
(public_name coq_makefile)
+ (package coq)
(modules coq_makefile)
(libraries coq.lib))
-(install
- (section lib)
- (files (CoqMakefile.in as tools/CoqMakefile.in)))
+(executable
+ (name coqc)
+ (public_name coqc)
+ (package coq)
+ (modules coqc)
+ (libraries coq.toplevel))
(executable
(name coqdep)
(public_name coqdep)
+ (package coq)
(modules coqdep_lexer coqdep_common coqdep)
(libraries coq.lib))
@@ -25,6 +34,7 @@
(executable
(name coqwc)
(public_name coqwc)
+ (package coq)
(modules coqwc)
(libraries))
@@ -33,11 +43,13 @@
(executable
(name coq_tex)
(public_name coq_tex)
+ (package coq)
(modules coq_tex)
(libraries str))
(executable
(name coq_dune)
(public_name coq_dune)
+ (package coq)
(modules coq_dune)
(libraries str))
diff --git a/tools/mkwinapp.ml b/tools/mkwinapp.ml
deleted file mode 100644
index 226302fb2d..0000000000
--- a/tools/mkwinapp.ml
+++ /dev/null
@@ -1,92 +0,0 @@
-(* OCaml-Win32
- * mkwinapp.ml
- * Copyright (c) 2002-2004 by Harry Chomsky
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Library General Public
- * License as published by the Free Software Foundation; either
- * version 2 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Library General Public License for more details.
- *
- * You should have received a copy of the GNU Library General Public
- * License along with this library; if not, write to the Free
- * Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
- *)
-
-(*********************************************************************
- * This program alters an .exe file to make it use the "windows subsystem"
- * instead of the "console subsystem". In other words, when Windows runs
- * the program, it will not create a console for it.
- *)
-
-(* Pierre Letouzey 23/12/2010 : modification to allow selecting the
- subsystem to use instead of just setting the windows subsystem *)
-
-(* This tool can be run directly via :
- ocaml unix.cma mkwinapp.ml [-set|-unset] <filename>
-*)
-
-exception Invalid_file_format
-
-let input_word ic =
- let lo = input_byte ic in
- let hi = input_byte ic in
- (hi lsl 8) + lo
-
-let find_pe_header ic =
- seek_in ic 0x3C;
- let peheader = input_word ic in
- seek_in ic peheader;
- if input_char ic <> 'P' then
- raise Invalid_file_format;
- if input_char ic <> 'E' then
- raise Invalid_file_format;
- peheader
-
-let find_optional_header ic =
- let peheader = find_pe_header ic in
- let coffheader = peheader + 4 in
- seek_in ic (coffheader + 16);
- let optsize = input_word ic in
- if optsize < 96 then
- raise Invalid_file_format;
- let optheader = coffheader + 20 in
- seek_in ic optheader;
- let magic = input_word ic in
- if magic <> 0x010B && magic <> 0x020B then
- raise Invalid_file_format;
- optheader
-
-let change flag ic oc =
- let optheader = find_optional_header ic in
- seek_out oc (optheader + 64);
- for i = 1 to 4 do
- output_byte oc 0
- done;
- output_byte oc (if flag then 2 else 3)
-
-let usage () =
- print_endline "Alters a Win32 executable file to use the Windows subsystem or not.";
- print_endline "Usage: mkwinapp [-set|-unset] <filename>";
- print_endline "Giving no option is equivalent to -set";
- exit 1
-
-let main () =
- let n = Array.length Sys.argv - 1 in
- if not (n = 1 || n = 2) then usage ();
- let flag =
- if n = 1 then true
- else if Sys.argv.(1) = "-set" then true
- else if Sys.argv.(1) = "-unset" then false
- else usage ()
- in
- let filename = Sys.argv.(n) in
- let f = Unix.openfile filename [Unix.O_RDWR] 0 in
- let ic = Unix.in_channel_of_descr f and oc = Unix.out_channel_of_descr f in
- change flag ic oc
-
-let _ = main ()
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 382c39d3f2..053a0435ce 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -14,11 +14,6 @@
let syntax_error lexbuf =
raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
- [@@@ocaml.warning "-3"] (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
- let uncapitalize = String.uncapitalize
-
- let capitalize = String.capitalize
- [@@@ocaml.warning "+3"]
}
let space = [' ' '\t' '\n' '\r']
@@ -31,7 +26,7 @@ let caml_low_ident = lowercase identchar*
rule mllib_list = parse
| uppercase+ { let s = Lexing.lexeme lexbuf in
s :: mllib_list lexbuf }
- | caml_up_ident { let s = uncapitalize (Lexing.lexeme lexbuf)
+ | caml_up_ident { let s = String.uncapitalize_ascii (Lexing.lexeme lexbuf)
in s :: mllib_list lexbuf }
| "*predef*" { mllib_list lexbuf }
| space+ { mllib_list lexbuf }
@@ -204,7 +199,7 @@ let mlpack_dependencies () =
List.iter
(fun (name,dirname) ->
let fullname = file_name name dirname in
- let modname = capitalize name in
+ let modname = String.capitalize_ascii name in
let deps = traite_fichier_modules fullname ".mlpack" in
let sdeps = String.concat " " deps in
let efullname = escape fullname in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 21:38:59 +0000