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/fake_ide.ml334
-rw-r--r--tools/mkwinapp.ml92
-rw-r--r--tools/ocamllibdep.mll9
16 files changed, 51 insertions, 608 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/fake_ide.ml b/tools/fake_ide.ml
deleted file mode 100644
index 0162011289..0000000000
--- a/tools/fake_ide.ml
+++ /dev/null
@@ -1,334 +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) *)
-(************************************************************************)
-
-(** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *)
-
-let error s =
- prerr_endline ("fake_id: error: "^s);
- exit 1
-
-let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp
-
-type coqtop = {
- xml_printer : Xml_printer.t;
- xml_parser : Xml_parser.t;
-}
-
-let print_error msg =
- Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg
-
-let base_eval_call ?(print=true) ?(fail=true) call coqtop =
- if print then prerr_endline (Xmlprotocol.pr_call call);
- let xml_query = Xmlprotocol.of_call call in
- Xml_printer.print coqtop.xml_printer xml_query;
- let rec loop () =
- let xml = Xml_parser.parse coqtop.xml_parser in
- if Xmlprotocol.is_feedback xml then
- loop ()
- else Xmlprotocol.to_answer call xml
- in
- let res = loop () in
- if print then prerr_endline (Xmlprotocol.pr_full_value call res);
- match res with
- | Interface.Fail (_,_,s) when fail -> print_error s; exit 1
- | Interface.Fail (_,_,s) as x -> print_error s; x
- | x -> x
-
-let eval_call c q = ignore(base_eval_call c q)
-
-module Parser = struct (* {{{ *)
-
- exception Err of string
- exception More
-
- type token =
- | Tok of string * string
- | Top of token list
-
- type grammar =
- | Alt of grammar list
- | Seq of grammar list
- | Opt of grammar
- | Item of (string * (string -> token * int))
-
- let eat_rex x = x, fun s ->
- if Str.string_match (Str.regexp x) s 0 then begin
- let m = Str.match_end () in
- let w = String.sub s 0 m in
- Tok(x,w), m
- end else raise (Err ("Regexp "^x^" not found in: "^s))
-
- let eat_balanced c =
- let c' = match c with
- | '{' -> '}' | '(' -> ')' | '[' -> ']' | _ -> assert false in
- let sc, sc' = String.make 1 c, String.make 1 c' in
- let name = sc ^ "..." ^ sc' in
- let unescape s =
- Str.global_replace (Str.regexp ("\\\\"^sc)) sc
- (Str.global_replace (Str.regexp ("\\\\"^sc')) sc' s) in
- name, fun s ->
- if s.[0] = c then
- let rec find n m =
- if String.length s <= m then raise More;
- if s.[m] = c' then
- if n = 0 then Tok (name, unescape (String.sub s 1 (m-1))), m+1
- else find (n-1) (m+1)
- else if s.[m] = c then find (n+1) (m+1)
- else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c then
- find n (m+2)
- else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c' then
- find n (m+2)
- else find n (m+1)
- in find ~-1 0
- else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s))
-
- let eat_blanks s = snd (eat_rex "[ \r\n\t]*") s
-
- let s = ref ""
-
- let parse g ic =
- let read_more () = s := !s ^ input_line ic ^ "\n" in
- let ensure_non_empty n = if n = String.length !s then read_more () in
- let cut_after s n = String.sub s n (String.length s - n) in
- let rec wrap f n =
- try
- ensure_non_empty n;
- let _, n' = eat_blanks (cut_after !s n) in
- ensure_non_empty n';
- let t, m = f (cut_after !s (n+n')) in
- let _, m' = eat_blanks (cut_after !s (n+n'+m)) in
- t, n+n'+m+m'
- with More -> read_more (); wrap f n in
- let rec aux n g res : token list * int =
- match g with
- | Item (_,f) ->
- let t, n = wrap f n in
- t :: res, n
- | Opt g ->
- (try let res', n = aux n g [] in Top (List.rev res') :: res, n
- with Err _ -> Top [] :: res, n)
- | Alt gl ->
- let rec fst = function
- | [] -> raise (Err ("No more alternatives for: "^cut_after !s n))
- | g :: gl ->
- try aux n g res
- with Err s -> fst gl in
- fst gl
- | Seq gl ->
- let rec all (res,n) = function
- | [] -> res, n
- | g :: gl -> all (aux n g res) gl in
- all (res,n) gl in
- let res, n = aux 0 g [] in
- s := cut_after !s n;
- List.rev res
-
- let clean s = Str.global_replace (Str.regexp "\n") "\\n" s
-
- let rec print g =
- match g with
- | Item (s,_) -> Printf.sprintf "%s" (clean s)
- | Opt g -> Printf.sprintf "[%s]" (print g)
- | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs))
- | Seq gs -> String.concat " " (List.map print gs)
-
- let rec print_toklist = function
- | [] -> ""
- | Tok(k,v) :: rest when k = v -> clean k ^ " " ^ print_toklist rest
- | Tok(k,v) :: rest -> clean k ^ " = \"" ^ clean v ^ "\" " ^ print_toklist rest
- | Top l :: rest -> print_toklist l ^ " " ^ print_toklist rest
-
-end (* }}} *)
-
-type sentence = {
- name : string;
- text : string;
- edit_id : int;
-}
-
-let doc : sentence Document.document = Document.create ()
-
-let tip_id () =
- try Document.tip doc
- with
- | Document.Empty -> Stateid.initial
- | Invalid_argument _ -> error "add_sentence on top of non assigned tip"
-
-let add_sentence =
- let edit_id = ref 0 in
- fun ?(name="") text ->
- let tip_id = tip_id () in
- decr edit_id;
- Document.push doc { name; text; edit_id = !edit_id };
- !edit_id, tip_id
-
-let print_document () =
- let ellipsize s =
- Str.global_replace (Str.regexp "^[\n ]*") ""
- (if String.length s > 20 then String.sub s 0 17 ^ "..."
- else s) in
- pperr_endline (
- (Document.print doc
- (fun b state_id { name; text } ->
- Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
- (if b then "*" else " ")
- name
- (Stateid.to_string (Option.default Stateid.dummy state_id))
- (ellipsize text)))))
-
-(* This module is the logic a GUI has to implement *)
-module GUILogic = struct
-
- let after_add = function
- | Interface.Fail (_,_,s) -> print_error s; exit 1
- | Interface.Good (id, (Util.Inl (), _)) ->
- Document.assign_tip_id doc id
- | Interface.Good (id, (Util.Inr tip, _)) ->
- Document.assign_tip_id doc id;
- Document.unfocus doc;
- ignore(Document.cut_at doc tip);
- print_document ()
-
- let at id id' _ = Stateid.equal id' id
-
- let after_edit_at (id,need_unfocus) = function
- | Interface.Fail (_,_,s) -> print_error s; exit 1
- | Interface.Good (Util.Inl ()) ->
- if need_unfocus then Document.unfocus doc;
- ignore(Document.cut_at doc id);
- print_document ()
- | Interface.Good (Util.Inr (stop_id,(start_id,tip))) ->
- if need_unfocus then Document.unfocus doc;
- ignore(Document.cut_at doc tip);
- Document.focus doc ~cond_top:(at start_id) ~cond_bot:(at stop_id);
- ignore(Document.cut_at doc id);
- print_document ()
-
- let get_id_pred pred =
- try Document.find_id doc pred
- with Not_found -> error "No state found"
-
- let get_id id = get_id_pred (fun _ { name } -> name = id)
-
- let after_fail coq = function
- | Interface.Fail (safe_id,_,s) ->
- prerr_endline "The command failed as expected";
- let to_id, need_unfocus =
- get_id_pred (fun id _ -> Stateid.equal id safe_id) in
- after_edit_at (to_id, need_unfocus)
- (base_eval_call (Xmlprotocol.edit_at to_id) coq)
- | Interface.Good _ -> error "The command was expected to fail but did not"
-
-end
-
-open GUILogic
-
-let eval_print l coq =
- let open Parser in
- let open Xmlprotocol in
- (* prerr_endline ("Interpreting: " ^ print_toklist l); *)
- match l with
- | [ Tok(_,"ADD"); Top []; Tok(_,phrase) ] ->
- let eid, tip = add_sentence phrase in
- after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq)
- | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] ->
- let eid, tip = add_sentence ~name phrase in
- after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq)
- | [ Tok(_,"GOALS"); ] ->
- eval_call (goals ()) coq
- | [ Tok(_,"FAILGOALS"); ] ->
- after_fail coq (base_eval_call ~fail:false (goals ()) coq)
- | [ Tok(_,"EDIT_AT"); Tok(_,id) ] ->
- let to_id, need_unfocus = get_id id in
- after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq)
- | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] ->
- eval_call (query (0,(phrase,tip_id()))) coq
- | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
- let to_id, _ = get_id id in
- eval_call (query (0,(phrase, to_id))) coq
- | [ Tok(_,"WAIT") ] ->
- eval_call (wait ()) coq
- | [ Tok(_,"JOIN") ] ->
- eval_call (status true) coq
- | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
- let to_id, _ = get_id id in
- if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
- else prerr_endline "Good tip"
- | Tok("#[^\n]*",_) :: _ -> ()
- | _ -> error "syntax error"
-
-let grammar =
- let open Parser in
- let eat_id = eat_rex "[a-zA-Z_][a-zA-Z0-9_]*" in
- let eat_phrase = eat_balanced '{' in
- Alt
- [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase]
- ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
- ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
- ; Seq [Item (eat_rex "WAIT")]
- ; Seq [Item (eat_rex "JOIN")]
- ; Seq [Item (eat_rex "GOALS")]
- ; Seq [Item (eat_rex "FAILGOALS")]
- ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ]
- ; Item (eat_rex "#[^\n]*")
- ]
-
-let read_command inc = Parser.parse grammar inc
-
-let usage () =
- error (Printf.sprintf
- "A fake coqide process talking to a coqtop -toploop coqidetop.\n\
- Usage: %s (file|-) [<coqtop>]\n\
- Input syntax is the following:\n%s\n"
- (Filename.basename Sys.argv.(0))
- (Parser.print grammar))
-
-module Coqide = Spawn.Sync ()
-
-let main =
- if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
- (Sys.Signal_handle
- (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
- let def_args = ["--xml_format=Ppcmds"] in
- let idetop_name = System.get_toplevel_path "coqidetop" in
- let coqtop_args, input_file = match Sys.argv with
- | [| _; f |] -> Array.of_list def_args, f
- | [| _; f; ct |] ->
- let ct = Str.split (Str.regexp " ") ct in
- Array.of_list (def_args @ ct), f
- | _ -> usage () in
- let inc = if input_file = "-" then stdin else open_in input_file in
- let coq =
- let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in
- let ip = Xml_parser.make (Xml_parser.SChannel cin) in
- let op = Xml_printer.make (Xml_printer.TChannel cout) in
- Xml_parser.check_eof ip false;
- { xml_printer = op; xml_parser = ip } in
- let init () =
- match base_eval_call ~print:false (Xmlprotocol.init None) coq with
- | Interface.Good id ->
- let dir = Filename.dirname input_file in
- let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in
- let eid, tip = add_sentence ~name:"initial" phrase in
- after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq)
- | Interface.Fail _ -> error "init call failed" in
- let finish () =
- match base_eval_call (Xmlprotocol.status true) coq with
- | Interface.Good _ -> exit 0
- | Interface.Fail (_,_,s) -> print_error s; exit 1 in
- (* The main loop *)
- init ();
- while true do
- let cmd = try read_command inc with End_of_file -> finish () in
- try eval_print cmd coq
- with e -> error ("Uncaught exception " ^ Printexc.to_string e)
- done
-
-(* vim:set foldmethod=marker: *)
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-04 11:27:03 +0000