From 6c4062ca13e6fb9e7d2dc93c70b545ccb22575de Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 18 Jun 2018 16:53:54 +0000 Subject: Archive the `gallina` tool --- .gitignore | 1 - CHANGES | 2 + Makefile.build | 8 -- Makefile.common | 4 +- Makefile.install | 2 +- configure.ml | 2 +- doc/sphinx/practical-tools/utilities.rst | 14 +--- man/gallina.1 | 74 ------------------ tools/CoqMakefile.in | 9 --- tools/gallina.ml | 63 ---------------- tools/gallina_lexer.mll | 126 ------------------------------- 11 files changed, 6 insertions(+), 299 deletions(-) delete mode 100644 man/gallina.1 delete mode 100644 tools/gallina.ml delete mode 100644 tools/gallina_lexer.mll diff --git a/.gitignore b/.gitignore index 6adbc9fb2..605629055 100644 --- a/.gitignore +++ b/.gitignore @@ -119,7 +119,6 @@ dev/ocamlweb-doc/lex.ml ide/coq_lex.ml ide/config_lexer.ml ide/utf8_convert.ml -tools/gallina_lexer.ml tools/coqwc.ml tools/coqdep_lexer.ml tools/ocamllibdep.ml diff --git a/CHANGES b/CHANGES index 6ad2cc548..2ccd5cb88 100644 --- a/CHANGES +++ b/CHANGES @@ -41,6 +41,8 @@ Tools COQFLAGS is now entirely separate from COQLIBS, so in custom Makefiles $(COQFLAGS) should be replaced by $(COQFLAGS) $(COQLIBS). +- Remove the gallina utility (extracts specification from Coq vernacular files). + Vernacular Commands - Removed deprecated commands Arguments Scope and Implicit Arguments diff --git a/Makefile.build b/Makefile.build index b85418243..49afa50b2 100644 --- a/Makefile.build +++ b/Makefile.build @@ -493,14 +493,6 @@ $(COQDEPBYTE): $(COQDEPCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(call ocamlbyte, $(SYSMOD)) -$(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) - $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,) - -$(GALLINABYTE): tools/gallina_lexer.cmo tools/gallina.cmo - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(call ocamlbyte,) - COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) diff --git a/Makefile.common b/Makefile.common index 5b1def40a..26523ec95 100644 --- a/Makefile.common +++ b/Makefile.common @@ -24,8 +24,6 @@ COQDEP:=bin/coqdep$(EXE) COQDEPBYTE:=bin/coqdep.byte$(EXE) COQMAKEFILE:=bin/coq_makefile$(EXE) COQMAKEFILEBYTE:=bin/coq_makefile.byte$(EXE) -GALLINA:=bin/gallina$(EXE) -GALLINABYTE:=bin/gallina.byte$(EXE) COQTEX:=bin/coq-tex$(EXE) COQTEXBYTE:=bin/coq-tex.byte$(EXE) COQWC:=bin/coqwc$(EXE) @@ -41,7 +39,7 @@ COQTIME_FILE_MAKER:=tools/TimeFileMaker.py COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py -TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ +TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ $(COQWORKMGR) TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) diff --git a/Makefile.install b/Makefile.install index 010e35d42..63a1b8b5e 100644 --- a/Makefile.install +++ b/Makefile.install @@ -138,7 +138,7 @@ endif install-coq-info: install-coq-manpages install-emacs install-latex -MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ +MANPAGES:=man/coq-tex.1 man/coqdep.1 \ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ man/coqwc.1 man/coqdoc.1 man/coqide.1 \ man/coq_makefile.1 man/coqchk.1 diff --git a/configure.ml b/configure.ml index b5d5a2419..5a5c34ec8 100644 --- a/configure.ml +++ b/configure.ml @@ -18,7 +18,7 @@ let vo_magic = 8891 let state_magic = 58891 let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; - "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] + "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"] let verbose = ref false (* for debugging this script *) diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5dba92429..64d4773a2 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -1000,21 +1000,9 @@ Proof-General is developed and distributed independently of the system |Coq|. It is freely available at ``_. -Module specification --------------------- - -Given a |Coq| vernacular file, the gallina filter extracts its -specification (inductive types declarations, definitions, type of -lemmas and theorems), removing the proofs parts of the file. The |Coq| -file ``file.v`` gives birth to the specification file ``file.g`` (where -the suffix ``.g`` stands for |Gallina|). - -See the man page of ``gallina`` for more details and options. - - Man pages --------- -There are man pages for the commands ``coqdep``, ``gallina`` and ``coq-tex``. Man +There are man pages for the commands ``coqdep`` and ``coq-tex``. Man pages are installed at installation time (see installation instructions in file ``INSTALL``, step 6). diff --git a/man/gallina.1 b/man/gallina.1 deleted file mode 100644 index f8879c457..000000000 --- a/man/gallina.1 +++ /dev/null @@ -1,74 +0,0 @@ -.TH COQ 1 "29 March 1995" "Coq tools" - -.SH NAME -gallina \- extracts specification from Coq vernacular files - -.SH SYNOPSIS -.B gallina -[ -.BI \- -] -[ -.BI \-stdout -] -[ -.BI \-nocomments -] -.I file ... - -.SH DESCRIPTION - -.B gallina -takes Coq files as arguments and builds the corresponding -specification files. -The Coq file -.IR foo.v \& -gives bearth to the specification file -.IR foo.g. \& -The suffix '.g' stands for Gallina. - -For that purpose, gallina removes all commands that follow a -"Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until it -reaches a command "Abort.", "Qed.", "Defined." or "Proof -<...>.". It also removes every "Hint", "Syntax", -"Immediate" or "Transparent" command. - -Files without the .v suffix are ignored. - - -.SH OPTIONS - -.TP -.BI \-stdout -Prints the result on standard output. -.TP -.BI \- -Coq source is taken on standard input. The result is printed on -standard output. -.TP -.BI \-nocomments -Comments are removed in the *.g file. - -.SH NOTES - -Nested comments are correctly handled. In particular, every command -"Qed." or "Abort." in a comment is not taken into account. - - -.SH BUGS - -Please report any bug to -.B coq@pauillac.inria.fr - - - - - - - - - - - - - diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8e60d3932..b8ce164a6 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -86,7 +86,6 @@ COQC ?= "$(COQBIN)coqc" COQTOP ?= "$(COQBIN)coqtop" COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" -GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" COQMKFILE ?= "$(COQBIN)coq_makefile" @@ -256,7 +255,6 @@ VO = vo VOFILES = $(VFILES:.v=.$(VO)) GLOBFILES = $(VFILES:.v=.glob) -GFILES = $(VFILES:.v=.g) HTMLFILES = $(VFILES:.v=.html) GHTMLFILES = $(VFILES:.v=.g.html) BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) @@ -442,8 +440,6 @@ all-mli.tex: $(MLIFILES:.mli=.cmi) $(HIDE)$(CAMLDOC) -latex \ -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) -gallina: $(GFILES) - all.ps: $(VFILES) $(SHOW)'COQDOC -ps $(GAL)' $(HIDE)$(COQDOC) \ @@ -564,7 +560,6 @@ clean:: $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) $(HIDE)rm -f $(VOFILES:.vo=.vio) - $(HIDE)rm -f $(GFILES) $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex $(HIDE)rm -f $(VFILES:.v=.glob) @@ -683,10 +678,6 @@ $(BEAUTYFILES): %.v.beautified: %.v $(SHOW)'BEAUTIFY $<' $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< -$(GFILES): %.g: %.v - $(SHOW)'GALLINA $<' - $(HIDE)$(GALLINA) $< - $(TEXFILES): %.tex: %.v $(SHOW)'COQDOC -latex $<' $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ diff --git a/tools/gallina.ml b/tools/gallina.ml deleted file mode 100644 index c7ff76bec..000000000 --- a/tools/gallina.ml +++ /dev/null @@ -1,63 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* begin - flush !chan_out; - close_in chan_in; - if not !option_stdout then close_out !chan_out - end - with Sys_error _ -> - () - -let traite_stdin () = - try - let buf = Lexing.from_channel stdin in - try - while true do Gallina_lexer.action buf done - with Fin_fichier -> - flush !chan_out - with Sys_error _ -> - () - -let _ = - let lg_command = Array.length Sys.argv in - if lg_command < 2 then begin - output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n"; - flush stderr; - exit 1 - end; - let treat = function - | "-" -> option_moins := true - | "-stdout" -> option_stdout := true - | "-nocomments" -> comments := false - | f -> - if Filename.check_suffix f ".v" then - vfiles := (Filename.chop_suffix f ".v") :: !vfiles - in - Array.iter treat Sys.argv; - if !option_moins then - traite_stdin () - else - List.iter traite_fichier !vfiles diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll deleted file mode 100644 index 1a594aebb..000000000 --- a/tools/gallina_lexer.mll +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 0 then comment lexbuf } - | "*)" [' ''\t']*'\n' { (if !comments then print (Lexing.lexeme lexbuf)); - comment_depth := pred !comment_depth; - if !comment_depth > 0 then comment lexbuf } - | eof { raise Fin_fichier } - | _ { (if !comments then print (Lexing.lexeme lexbuf)); - comment lexbuf } - -and skip_comment = parse - | "(*" { comment_depth := succ !comment_depth; skip_comment lexbuf } - | "*)" { comment_depth := pred !comment_depth; - if !comment_depth > 0 then skip_comment lexbuf } - | eof { raise Fin_fichier } - | _ { skip_comment lexbuf } - -and body_def = parse - | [^'.']* ":=" { print (Lexing.lexeme lexbuf); () } - | _ { print (Lexing.lexeme lexbuf); body lexbuf } - -and body = parse - | enddot { print ".\n"; skip_proof lexbuf } - | ":=" { print ".\n"; skip_proof lexbuf } - | "(*" { print "(*"; comment_depth := 1; - comment lexbuf; body lexbuf } - | eof { raise Fin_fichier } - | _ { print (Lexing.lexeme lexbuf); body lexbuf } - -and body_pgm = parse - | enddot { print ".\n"; skip_proof lexbuf } - | "(*" { print "(*"; comment_depth := 1; - comment lexbuf; body_pgm lexbuf } - | eof { raise Fin_fichier } - | _ { print (Lexing.lexeme lexbuf); body_pgm lexbuf } - -and skip_until_point = parse - | '.' '\n' { () } - | enddot { end_of_line lexbuf } - | "(*" { comment_depth := 1; - skip_comment lexbuf; skip_until_point lexbuf } - | eof { raise Fin_fichier } - | _ { skip_until_point lexbuf } - -and end_of_line = parse - | [' ' '\t' ]* { end_of_line lexbuf } - | '\n' { () } - | eof { raise Fin_fichier } - | _ { print (Lexing.lexeme lexbuf) } - -and skip_proof = parse - | "Save" space - { skip_until_point lexbuf } - | "Qed." { end_of_line lexbuf } - | "Qed" space - { skip_until_point lexbuf } - | "Defined." { end_of_line lexbuf } - | "Defined" space - { skip_until_point lexbuf } - | "Abort." { end_of_line lexbuf } - | "Abort" space - { skip_until_point lexbuf } - | "Proof" space { skip_until_point lexbuf } - | "Proof" [' ' '\t']* '.' { skip_proof lexbuf } - | "(*" { comment_depth := 1; - skip_comment lexbuf; skip_proof lexbuf } - | eof { raise Fin_fichier } - | _ { skip_proof lexbuf } -- cgit v1.2.3