diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/README.emacs | 31 | ||||
| -rwxr-xr-x | tools/check-translate | 23 | ||||
| -rw-r--r-- | tools/coq-sl.sty | 37 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 43 | ||||
| -rw-r--r-- | tools/coqc.ml | 8 | ||||
| -rw-r--r-- | tools/coqdep.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/dune | 6 | ||||
| -rw-r--r-- | tools/dune | 21 | ||||
| -rw-r--r-- | tools/mkwinapp.ml | 92 |
9 files changed, 28 insertions, 235 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..691f37b414 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 @@ -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/coqdoc/dune b/tools/coqdoc/dune index 8e05c7d97e..b20d9f9b2e 100644 --- a/tools/coqdoc/dune +++ b/tools/coqdoc/dune @@ -1,3 +1,9 @@ +(install + (section lib) + (files + (coqdoc.css as tools/coqdoc/coqdoc.css) + (coqdoc.sty as tools/coqdoc/coqdoc.sty))) + (executable (name main) (public_name coqdoc) diff --git a/tools/dune b/tools/dune index 05a620fb07..20048fde52 100644 --- a/tools/dune +++ b/tools/dune @@ -1,8 +1,11 @@ -(executable - (name coqc) - (public_name coqc) - (modules coqc) - (libraries coq.toplevel)) +(install + (section lib) + (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) @@ -10,9 +13,11 @@ (modules coq_makefile) (libraries coq.lib)) -(install - (section lib) - (files (CoqMakefile.in as tools/CoqMakefile.in))) +(executable + (name coqc) + (public_name coqc) + (modules coqc) + (libraries coq.toplevel)) (executable (name coqdep) 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 () |