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 --- tools/CoqMakefile.in | 9 ---- tools/gallina.ml | 63 ------------------------ tools/gallina_lexer.mll | 126 ------------------------------------------------ 3 files changed, 198 deletions(-) delete mode 100644 tools/gallina.ml delete mode 100644 tools/gallina_lexer.mll (limited to 'tools') 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