Merge PR #7921: Archive the `gallina` tool

11 files changed, 6 insertions, 299 deletions

diff --git a/.gitignore b/.gitignore
index 1eee3f94f..466f4c1a7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -120,7 +120,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 3ec53fad2..76e8f8929 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,6 +45,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 5fd3bd873..cd145ae64 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -515,14 +515,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 bb6302a98..96d0d2ed8 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 21015d336..91870aff7 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 b264a2652..fde0a409c 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 `<https://proofgeneral.github.io/>`_.
 
 
-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 2ebe4aba7..872a73282 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       *)
-(* <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)         *)
-(************************************************************************)
-
-open Gallina_lexer
-
-let vfiles = ref ([] : string list)
-
-let option_moins = ref false
-
-let option_stdout = ref false
-
-let traite_fichier f =
-  try
-    let chan_in = open_in (f^".v") in
-    let buf = Lexing.from_channel chan_in in
-    if not !option_stdout then chan_out := open_out (f ^ ".g");
-    try
-      while true do Gallina_lexer.action buf done
-    with Fin_fichier -> 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       *)
-(* <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)         *)
-(************************************************************************)
-
-{
-
- let chan_out = ref stdout
-
- let comment_depth = ref 0
- let cRcpt = ref 0
- let comments = ref true
- let print s = output_string !chan_out s
-
- exception Fin_fichier
-
-}
-
-let space = [' ' '\t' '\n' '\r']
-let enddot = '.' (' ' | '\t' | '\n' | '\r' | eof)
-
-rule action = parse
-  | "Theorem" space { print "Theorem "; body lexbuf;
-  	              cRcpt := 1; action lexbuf }
-  | "Lemma" space   { print "Lemma ";   body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Fact" space    { print "Fact ";   body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Remark" space  { print "Remark ";  body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Goal" space    { print "Goal ";    body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Correctness" space { print "Correctness "; body_pgm lexbuf;
-      	       	          cRcpt := 1; action lexbuf }
-  | "Definition" space  { print "Definition "; body_def lexbuf;
-			  cRcpt := 1; action lexbuf }
-  | "Hint" space        { skip_until_point lexbuf ; action lexbuf }
-  | "Hints" space        { skip_until_point lexbuf ; action lexbuf }
-  | "Transparent" space { skip_until_point lexbuf ; action lexbuf }
-  | "Immediate"	space   { skip_until_point lexbuf ; action lexbuf }
-  | "Syntax" space      { skip_until_point lexbuf ; action lexbuf }
-  | "(*"      { (if !comments then print "(*");
-		comment_depth := 1;
-      	        comment lexbuf;
-		cRcpt := 0; action lexbuf }
-  | [' ' '\t']* '\n'      { if !cRcpt < 2 then print "\n";
-      	       	       	    cRcpt := !cRcpt+1; action lexbuf}
-  | eof       { (raise Fin_fichier : unit)}
-  | _         { print (Lexing.lexeme lexbuf); cRcpt := 0; action lexbuf }
-
-and comment = parse
-  | "(*"  { (if !comments then print "(*");
-      	    comment_depth := succ !comment_depth; comment lexbuf }
-  | "*)"  { (if !comments then print "*)");
-      	    comment_depth := pred !comment_depth;
-            if !comment_depth > 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 }