diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 81 | ||||
| -rw-r--r-- | tools/README.emacs | 31 | ||||
| -rw-r--r-- | tools/TimeFileMaker.py | 37 | ||||
| -rwxr-xr-x | tools/check-translate | 23 | ||||
| -rw-r--r-- | tools/coq-font-lock.el | 137 | ||||
| -rw-r--r-- | tools/coq-sl.sty | 37 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 283 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 64 | ||||
| -rw-r--r-- | tools/coqc.ml | 14 | ||||
| -rw-r--r-- | tools/coqdep.ml | 58 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 63 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 2 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mll | 9 | ||||
| -rw-r--r-- | tools/coqdoc/alpha.ml | 10 | ||||
| -rw-r--r-- | tools/coqdoc/dune | 14 | ||||
| -rw-r--r-- | tools/coqdoc/index.ml | 22 | ||||
| -rw-r--r-- | tools/coqdoc/index.mli | 2 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 17 | ||||
| -rw-r--r-- | tools/coqworkmgr.ml | 2 | ||||
| -rw-r--r-- | tools/dune | 55 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 346 | ||||
| -rw-r--r-- | tools/gallina-db.el | 240 | ||||
| -rw-r--r-- | tools/gallina-syntax.el | 979 | ||||
| -rw-r--r-- | tools/gallina.el | 142 | ||||
| -rw-r--r-- | tools/gallina.ml | 63 | ||||
| -rw-r--r-- | tools/gallina_lexer.mll | 126 | ||||
| -rw-r--r-- | tools/inferior-coq.el | 324 | ||||
| -rw-r--r-- | tools/mkwinapp.ml | 92 | ||||
| -rw-r--r-- | tools/ocamllibdep.mll | 25 |
29 files changed, 551 insertions, 2747 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f6539d80be..b673225e40 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -20,7 +20,7 @@ include @CONF_FILE@ VFILES := $(COQMF_VFILES) MLIFILES := $(COQMF_MLIFILES) MLFILES := $(COQMF_MLFILES) -ML4FILES := $(COQMF_ML4FILES) +MLGFILES := $(COQMF_MLGFILES) MLPACKFILES := $(COQMF_MLPACKFILES) MLLIBFILES := $(COQMF_MLLIBFILES) CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES) @@ -36,10 +36,6 @@ LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) -CAMLP5O := $(COQMF_CAMLP5O) -CAMLP5BIN := $(COQMF_CAMLP5BIN) -CAMLP5LIB := $(COQMF_CAMLP5LIB) -CAMLP5OPTIONS := $(COQMF_CAMLP5OPTIONS) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) @@ -65,20 +61,20 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= TIMECMD?= -# Use /usr/bin/env time on linux, gtime on Mac OS +# Use command time on linux, gtime on Mac OS TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) -ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) else ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) else -STDTIME?=time +STDTIME?=command time endif endif else -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +STDTIME?=command time -f $(TIMEFMT) endif # Coq binaries @@ -86,8 +82,8 @@ COQC ?= "$(COQBIN)coqc" COQTOP ?= "$(COQBIN)coqtop" COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" -GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" +COQPP ?= "$(COQBIN)coqpp" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts @@ -98,7 +94,7 @@ BEFORE ?= AFTER ?= # FIXME this should be generated by Coq (modules already linked by Coq) -CAMLDONTLINK=camlp5.gramlib,unix,str +CAMLDONTLINK=unix,str # OCaml binaries CAMLC ?= "$(OCAMLFIND)" ocamlc -c @@ -191,22 +187,11 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) # ocamldoc fails with unknown argument otherwise CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) -# FIXME This should be generated by Coq -GRAMMARS:=grammar.cma -CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo - -CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) -ifeq (,$(CAMLLIB)) -PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") -else -PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl' -endif - ifneq (,$(TIMING)) TIMING_ARG=-time ifeq (after,$(TIMING)) @@ -227,7 +212,7 @@ ifdef DSTROOT DESTDIR := $(DSTROOT) endif -concat_path = $(if $(1),$(1)/$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)) +concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2)) COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib) COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib) @@ -242,6 +227,7 @@ VDFILE := .coqdeps ALLSRCFILES := \ $(ML4FILES) \ + $(MLGFILES) \ $(MLFILES) \ $(MLPACKFILES) \ $(MLLIBFILES) \ @@ -256,7 +242,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)) @@ -264,6 +249,7 @@ TEXFILES = $(VFILES:.v=.tex) GTEXFILES = $(VFILES:.v=.g.tex) CMOFILES = \ $(ML4FILES:.ml4=.cmo) \ + $(MLGFILES:.mlg=.cmo) \ $(MLFILES:.ml=.cmo) \ $(MLPACKFILES:.mlpack=.cmo) CMXFILES = $(CMOFILES:.cmo=.cmx) @@ -279,7 +265,7 @@ CMXSFILES = \ $(MLPACKFILES:.mlpack=.cmxs) \ $(CMXAFILES:.cmxa=.cmxs) \ $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs)) + $(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) # files that are packed into a plugin (no extension) PACKEDFILES = \ @@ -345,19 +331,19 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: print-pretty-timed:: $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) ifeq (,$(BEFORE)) print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else ifeq (,$(AFTER)) print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: @@ -382,7 +368,7 @@ real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) .PHONY: real-all real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONE: real-all.timing.diff +.PHONY: real-all.timing.diff bytefiles: $(CMOFILES) $(CMAFILES) .PHONY: bytefiles @@ -442,8 +428,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) \ @@ -559,12 +543,12 @@ clean:: $(HIDE)rm -f $(CMXSFILES) $(HIDE)rm -f $(CMOFILES:.cmo=.o) $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(MLGFILES:.mlg=.ml) $(HIDE)rm -f $(ALLDFILES) $(HIDE)rm -f $(NATIVEFILES) $(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) @@ -607,11 +591,17 @@ $(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< -$(MLFILES:.ml=.cmo): %.cmo: %.ml +$(MLGFILES:.mlg=.ml): %.ml: %.mlg + $(SHOW)'COQPP $<' + $(HIDE)$(COQPP) $< + +# Stupid hack around a deficient syntax: we cannot concatenate two expansions +$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml $(SHOW)'CAMLC -c $<' $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< -$(MLFILES:.ml=.cmx): %.cmx: %.ml +# Same hack +$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< @@ -652,7 +642,7 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ # This rule is for _CoqProject with no .mllib nor .mlpack -$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -shared -o $@ $< @@ -683,10 +673,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 $@ @@ -717,6 +703,9 @@ endif redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) +GENMLFILES:=$(MLGFILES:.mlg=.ml) $(ML4FILES:.ml4=.ml) +$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) + $(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli $(SHOW)'CAMLDEP $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) @@ -725,6 +714,10 @@ $(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 $(SHOW)'CAMLDEP -pp $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok) +$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml $(SHOW)'CAMLDEP $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) @@ -765,10 +758,6 @@ printenv:: @echo 'COQLIB = $(COQLIB)' @echo 'DOCDIR = $(DOCDIR)' @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'CAMLP5O = $(CAMLP5O)' - @echo 'CAMLP5BIN = $(CAMLP5BIN)' - @echo 'CAMLP5LIB = $(CAMLP5LIB)' - @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)' @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' 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/TimeFileMaker.py b/tools/TimeFileMaker.py index 0d24332f1e..8564aeff64 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -1,6 +1,9 @@ -#!/usr/bin/env python from __future__ import with_statement +from __future__ import division +from __future__ import unicode_literals +from __future__ import print_function import os, sys, re +from io import open # This script parses the output of `make TIMED=1` into a dictionary # mapping names of compiled files to the number of minutes and seconds @@ -8,7 +11,7 @@ import os, sys, re STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') STRIP_REP = r'\1' -INFINITY = '\xe2\x88\x9e' +INFINITY = '\u221e' def parse_args(argv, USAGE, HELP_STRING): sort_by = 'auto' @@ -27,7 +30,7 @@ def parse_args(argv, USAGE, HELP_STRING): def reformat_time_string(time): seconds, milliseconds = time.split('.') seconds = int(seconds) - minutes, seconds = int(seconds / 60), seconds % 60 + minutes, seconds = divmod(seconds, 60) return '%dm%02d.%ss' % (minutes, seconds, milliseconds) def get_times(file_name): @@ -40,7 +43,7 @@ def get_times(file_name): if file_name == '-': lines = sys.stdin.read() else: - with open(file_name, 'r') as f: + with open(file_name, 'r', encoding="utf-8") as f: lines = f.read() reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) times = reg.findall(lines) @@ -60,7 +63,7 @@ def get_single_file_times(file_name): if file_name == '-': lines = sys.stdin.read() else: - with open(file_name, 'r') as f: + with open(file_name, 'r', encoding="utf-8") as f: lines = f.read() reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE) times = reg.findall(lines) @@ -101,7 +104,7 @@ def from_seconds(seconds, signed=False): ''' sign = ('-' if seconds < 0 else '+') if signed else '' seconds = abs(seconds) - minutes = int(seconds) / 60 + minutes = int(seconds) // 60 seconds -= minutes * 60 full_seconds = int(seconds) partial_seconds = int(100 * (seconds - full_seconds)) @@ -112,7 +115,8 @@ def sum_times(times, signed=False): Takes the values of an output from get_times, parses the time strings, and returns their sum, in the same string format. ''' - return from_seconds(sum(map(to_seconds, times)), signed=signed) + # sort the times before summing because floating point addition is not associative + return from_seconds(sum(sorted(map(to_seconds, times))), signed=signed) def format_percentage(num, signed=True): sign = ('-' if num < 0 else '+') if signed else '' @@ -141,20 +145,21 @@ def make_diff_table_string(left_times_dict, right_times_dict, for name, lseconds, rseconds in prediff_times) # update to sort by approximate difference, first get_key_abs = make_sorting_key(all_names_dict, descending=descending) - get_key_diff = (lambda name: fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending)) + get_key_diff_float = (lambda name: fix_sign_for_sorting(to_seconds(diff_times_dict[name]), descending=descending)) + get_key_diff_absint = (lambda name: fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending)) if sort_by == 'absolute': get_key = get_key_abs elif sort_by == 'diff': - get_key = get_key_diff + get_key = get_key_diff_float else: # sort_by == 'auto' - get_key = (lambda name: (get_key_diff(name), get_key_abs(name))) + get_key = (lambda name: (get_key_diff_absint(name), get_key_abs(name))) names = sorted(all_names_dict.keys(), key=get_key) #names = get_sorted_file_list_from_times_dict(all_names_dict, descending=descending) # set the widths of each of the columns by the longest thing to go in that column left_sum = sum_times(left_times_dict.values()) right_sum = sum_times(right_times_dict.values()) - left_sum_float = sum(map(to_seconds, left_times_dict.values())) - right_sum_float = sum(map(to_seconds, right_times_dict.values())) + left_sum_float = sum(sorted(map(to_seconds, left_times_dict.values()))) + right_sum_float = sum(sorted(map(to_seconds, right_times_dict.values()))) diff_sum = from_seconds(left_sum_float - right_sum_float, signed=True) percent_diff_sum = (format_percentage((left_sum_float - right_sum_float) / right_sum_float) if right_sum_float > 0 else 'N/A') @@ -203,8 +208,12 @@ def make_table_string(times_dict, def print_or_write_table(table, files): if len(files) == 0 or '-' in files: - print(table) + try: + binary_stdout = sys.stdout.buffer + except AttributeError: + binary_stdout = sys.stdout + print(table.encode("utf-8"), file=binary_stdout) for file_name in files: if file_name != '-': - with open(file_name, 'w') as f: + with open(file_name, 'w', encoding="utf-8") as f: f.write(table) 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-font-lock.el b/tools/coq-font-lock.el deleted file mode 100644 index 068e640025..0000000000 --- a/tools/coq-font-lock.el +++ /dev/null @@ -1,137 +0,0 @@ -;; coq-font-lock.el --- Coq syntax highlighting for Emacs - compatibilty code -;; Pierre Courtieu, may 2009 -;; -;; Authors: Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> - -;; This is copy paste from ProofGeneral by David Aspinall -;; <David.Aspinall@ed.ac.uk>. ProofGeneral is under GPL and Copyright -;; (C) LFCS Edinburgh. - - -;;; Commentary: -;; This file contains the code necessary to coq-syntax.el and -;; coq-db.el from ProofGeneral. It is also pocked from ProofGeneral. - - -;;; History: -;; First created from ProofGeneral may 28th 2009 - - -;;; Code: - -(setq coq-version-is-V8-1 t) -(defun coq-build-regexp-list-from-db (db &optional filter) - "Take a keyword database DB and return the list of regexps for font-lock. -If non-nil Optional argument FILTER is a function applying to each line of DB. -For each line if FILTER returns nil, then the keyword is not added to the -regexp. See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l)) (tl (cdr l)) ; hd is the first infos list - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - ) - ;; TODO delete doublons - (when (and e5 (or (not filter) (funcall filter hd))) - (setq res (nconc res (list e5)))) ; careful: nconc destructive! - (setq l tl))) - res - )) -(defun filter-state-preserving (l) - ; checkdoc-params: (l) - "Not documented." - (not (nth 3 l))) ; fourth argument is nil --> state preserving command - -(defun filter-state-changing (l) - ; checkdoc-params: (l) - "Not documented." - (nth 3 l)) ; fourth argument is nil --> state preserving command - -;; Generic font-lock - -(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" - "A regular expression for parsing identifiers.") - -;; For font-lock, we treat ,-separated identifiers as one identifier -;; and refontify commata using \{proof-zap-commas}. - -(defun proof-anchor-regexp (e) - "Anchor (\\`) and group the regexp E." - (concat "\\`\\(" e "\\)")) - -(defun proof-ids (proof-id &optional sepregexp) - "Generate a regular expression for separated lists of identifiers PROOF-ID. -Default is comma separated, or SEPREGEXP if set." - (concat proof-id "\\(\\s-*" (or sepregexp ",") "\\s-*" - proof-id "\\)*")) - -(defun proof-ids-to-regexp (l) - "Maps a non-empty list of tokens `L' to a regexp matching any element." - (if (featurep 'xemacs) - (mapconcat (lambda (s) (concat "\\_<" s "\\_>")) l "\\|") ;; old version - (concat "\\_<\\(?:" (mapconcat 'identity l "\\|") "\\)\\_>"))) - -;; TODO: get rid of this list. Does 'default work widely enough -;; by now? -(defconst pg-defface-window-systems - '(x ;; bog standard - mswindows ;; Windows - w32 ;; Windows - gtk ;; gtk emacs (obsolete?) - mac ;; used by Aquamacs - carbon ;; used by Carbon XEmacs - ns ;; NeXTstep Emacs (Emacs.app) - x-toolkit) ;; possible catch all (but probably not) - "A list of possible values for variable `window-system'. -If you are on a window system and your value of variable -`window-system' is not listed here, you may not get the correct -syntax colouring behaviour.") - -(defmacro proof-face-specs (bl bd ow) - "Return a spec for `defface' with BL for light bg, BD for dark, OW o/w." - `(append - (apply 'append - (mapcar - (lambda (ty) (list - (list (list (list 'type ty) '(class color) - (list 'background 'light)) - (quote ,bl)) - (list (list (list 'type ty) '(class color) - (list 'background 'dark)) - (quote ,bd)))) - pg-defface-window-systems)) - (list (list t (quote ,ow))))) - -;;A new face for tactics -(defface coq-solve-tactics-face - (proof-face-specs - (:foreground "forestgreen" t) ; for bright backgrounds - (:foreground "forestgreen" t) ; for dark backgrounds - ()) ; for black and white - "Face for names of closing tactics in proof scripts." - :group 'proof-faces) - -;;A new face for tactics which fail when they don't kill the current goal -(defface coq-solve-tactics-face - (proof-face-specs - (:foreground "red" t) ; for bright backgrounds - (:foreground "red" t) ; for dark backgrounds - ()) ; for black and white - "Face for names of closing tactics in proof scripts." - :group 'proof-faces) - - -(defconst coq-solve-tactics-face 'coq-solve-tactics-face - "Expression that evaluates to a face. -Required so that 'proof-solve-tactics-face is a proper facename") - -(defconst proof-tactics-name-face 'coq-solve-tactics-face) -(defconst proof-tacticals-name-face 'coq-solve-tactics-face) - -(provide 'coq-font-lock) -;;; coq-font-lock.el ends here 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 new file mode 100644 index 0000000000..84850e7158 --- /dev/null +++ b/tools/coq_dune.ml @@ -0,0 +1,283 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(* LICENSE NOTE: This file is dually MIT/LGPL 2.1+ licensed. MIT license: + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + *) + +(* coq_dune: generate dune build rules for .vo files *) +(* *) +(* At some point this file will become a Dune plugin, so it is very *) +(* important that this file can be bootstrapped with: *) +(* *) +(* ocamlfind ocamlopt -linkpkg -package str coq_dune.ml -o coq_dune *) + +open Format + +(* Keeping this file self-contained as it is a "bootstrap" utility *) +(* Is OCaml missing these basic functions in the stdlib? *) +module Aux = struct + + let option_iter f o = match o with + | Some x -> f x + | None -> () + + let option_cata d f o = match o with + | Some x -> f x + | None -> d + + let list_compare f = let rec lc x y = match x, y with + | [], [] -> 0 + | [], _ -> -1 + | _, [] -> 1 + | x::xs, y::ys -> let r = f x y in if r = 0 then lc xs ys else r + in lc + + let rec pp_list pp sep fmt l = match l with + | [] -> () + | [l] -> fprintf fmt "%a" pp l + | x::xs -> fprintf fmt "%a%a%a" pp x sep () (pp_list pp sep) xs + + let rec pmap f l = match l with + | [] -> [] + | x :: xs -> + begin match f x with + | None -> pmap f xs + | Some r -> r :: pmap f xs + end + + let sep fmt () = fprintf fmt "@;" + + (* Creation of paths, aware of the platform separator. *) + let bpath l = String.concat Filename.dir_sep l + + module DirOrd = struct + type t = string list + let compare = list_compare String.compare + end + + module DirMap = Map.Make(DirOrd) + + (* Functions available in newer OCaml versions *) + (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *) + module Legacy = struct + + + (* Fix once we move to OCaml >= 4.06.0 *) + let list_init len f = + let rec init_aux i n f = + if i >= n then [] + else let r = f i in r :: init_aux (i+1) n f + in init_aux 0 len f + + (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *) + let dirmap_update key f map = + match begin + try f (Some (DirMap.find key map)) + with Not_found -> f None + end with + | None -> DirMap.remove key map + | Some x -> DirMap.add key x map + + end + + let add_map_list key elem map = + (* Move to Dirmap.update once we require OCaml >= 4.06.0 *) + Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map + +end + +open Aux + +(* Once this is a Dune plugin the flags will be taken from the env *) +module Options = struct + + type flag = { + enabled : bool; + cmd : string; + } + + let all_opts = + [ { enabled = false; cmd = "-debug"; } + ; { enabled = false; cmd = "-native_compiler"; } + ] + + let build_coq_flags () = + let popt o = if o.enabled then Some o.cmd else None in + String.concat " " @@ pmap popt all_opts +end + +type vodep = { + target: string; + deps : string list; +} + +type ldep = | VO of vodep | ML4 of string | MLG of string +type ddir = ldep list DirMap.t + +(* Filter `.vio` etc... *) +let filter_no_vo = + List.filter (fun f -> Filename.check_suffix f ".vo") + +(* We could have coqdep to output dune files directly *) + +let gen_sub n = + (* Move to List.init once we can depend on OCaml >= 4.06.0 *) + bpath @@ Legacy.list_init n (fun _ -> "..") + +let pp_rule fmt targets deps action = + (* Special printing of the first rule *) + let ppl = pp_list pp_print_string sep in + let pp_deps fmt l = match l with + | [] -> + () + | x :: xs -> + fprintf fmt "(:pp-file %s)%a" x sep (); + pp_list pp_print_string sep fmt xs + in + fprintf fmt + "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n" + ppl targets pp_deps deps pp_print_string action + +(* Generate the dune rule: *) +let pp_vo_dep dir fmt vo = + let depth = List.length dir in + let sdir = gen_sub depth in + (* All files except those in Init implicitly depend on the Prelude, we account for it here. *) + let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", [bpath ["theories";"Init";"Prelude.vo"]] in + (* Coq flags *) + let cflag = Options.build_coq_flags () in + (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) + let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in + (* The source file is also corrected as we will call coqtop from the top dir *) + let source = bpath (dir @ [Filename.(remove_extension vo.target) ^ ".v"]) in + (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) + let libflag = "-coqlib %{project_root}" in + (* The final build rule *) + let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -compile %s))" libflag eflag cflag source in + pp_rule fmt [vo.target] deps action + +let pp_ml4_dep _dir fmt ml = + 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 = Filename.(remove_extension ml) ^ ".ml" in + let ml4_rule = "(run coqpp %{pp-file})" in + pp_rule fmt [target] [ml] ml4_rule + +let pp_dep dir fmt oo = match oo with + | VO vo -> pp_vo_dep dir fmt vo + | ML4 f -> pp_ml4_dep dir fmt f + | MLG f -> pp_mlg_dep dir fmt f + +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 (bpath [itarget;tg]) in + 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 + the install specification. *) +let record_dune d ff = + let sd = bpath d in + if Sys.file_exists sd && Sys.is_directory sd then + let out = open_out (bpath [sd;"dune"]) in + let fmt = formatter_of_out_channel out in + if List.nth d 0 = "plugins" then + fprintf fmt "(include plugin_base.dune)@\n"; + out_install fmt d ff; + List.iter (pp_dep d fmt) ff; + fprintf fmt "%!"; + close_out out + else + eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd + +(* File Scanning *) +let choose_ml4g_form f = + if Filename.check_suffix f ".ml4" then ML4 f + else MLG f + +let scan_mlg4 m d = + let dir = ["plugins"; d] in + let m = DirMap.add dir [] m in + let ml4 = Sys.(List.filter (fun f -> Filename.(check_suffix f ".ml4" || check_suffix f ".mlg")) + Array.(to_list @@ readdir (bpath dir))) in + List.fold_left (fun m f -> add_map_list ["plugins"; d] (choose_ml4g_form f) m) m ml4 + +let scan_plugins m = + let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in + let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in + List.fold_left scan_mlg4 m dirs + +(* Process .vfiles.d and generate a skeleton for the dune file *) +let parse_coqdep_line l = + match Str.(split (regexp ":") l) with + | [targets;deps] -> + let targets = Str.(split (regexp "[ \t]+") targets) in + let deps = Str.(split (regexp "[ \t]+") deps) in + let targets = filter_no_vo targets in + begin match targets with + | [target] -> + let dir, target = Filename.(dirname target, basename target) in + (* coqdep outputs with the '/' directory separator regardless of + the platform. Anyways, I hope we can link to coqdep instead + of having to parse its output soon, that should solve this + kind of issues *) + Some (String.split_on_char '/' dir, VO { target; deps; }) + (* Otherwise a vio file, we ignore *) + | _ -> None + end + (* Strange rule, we ignore *) + | _ -> None + +let rec read_vfiles ic map = + try + let rule = parse_coqdep_line (input_line ic) in + (* Add vo_entry to its corresponding map entry *) + let map = option_cata map (fun (dir, vo) -> add_map_list dir vo map) rule in + read_vfiles ic map + with End_of_file -> map + +let out_map map = + DirMap.iter record_dune map + +let exec_ifile f = + match Array.length Sys.argv with + | 1 -> f stdin + | 2 -> + let ic = open_in Sys.argv.(1) in + (try f ic with _ -> close_in ic) + | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1 + +let _ = + exec_ifile (fun ic -> + let map = scan_plugins DirMap.empty in + let map = read_vfiles ic map in + out_map map) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 6cd520d607..8560bac786 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -31,11 +31,22 @@ let rec print_prefix_list sep = function | x :: l -> print sep; print x; print_prefix_list sep l | [] -> () -let usage_common () = +let usage_coq_makefile () = + output_string stderr "Usage summary:\ +\n\ +\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ +\n ... [any] ... [-extra[-phony] result dependencies command]\ +\n ... [-I dir] ... [-R physicalpath logicalpath]\ +\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ +\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ +\n [-h] [--help]\ +\n"; output_string stderr "\ +\nFull list of options:\ +\n\ \n[file.v]: Coq file to be compiled\ \n[file.ml[i4]?]: Objective Caml file to be compiled\ -\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ +\n[file.ml{lib,pack}]: ocamlbuild-style file that describes a Objective Caml\ \n library/module\ \n[any] : subdirectory that should be \"made\" and has a Makefile itself\ \n to do so. Very fragile and discouraged.\ @@ -48,7 +59,7 @@ let usage_common () = \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ \n as a dependencies of an already defined target \"foo\".\ \n[-I dir]: look for Objective Caml dependencies in \"dir\"\ -\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ +\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\ \n starting from \"physicalpath\". The logical path associated to the\ \n physical path is \"logicalpath\".\ \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ @@ -61,25 +72,6 @@ let usage_common () = \n[-install opt]: where opt is \"user\" to force install into user directory,\ \n \"none\" to build a makefile with no install target or\ \n \"global\" to force install in $COQLIB directory\ -\n" - -let usage_coq_project () = - output_string stderr "Available arguments:"; - usage_common (); - exit 1 - -let usage_coq_makefile () = - output_string stderr "Usage summary:\ -\n\ -\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ -\n ... [any] ... [-extra[-phony] result dependencies command]\ -\n ... [-I dir] ... [-R physicalpath logicalpath]\ -\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ -\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ -\n [-h] [--help]\ -\n"; - usage_common (); - output_string stderr "\ \n[-f file]: take the contents of file as arguments\ \n[-o file]: output should go in file file (recommended)\ \n Output file outside the current directory is forbidden.\ @@ -215,10 +207,10 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } = let windrive s = if Coq_config.arch_is_win32 && Str.(string_match (regexp "^[a-zA-Z]:") s 0) then Str.matched_string s - else s + else "" ;; -let generate_conf_coq_config oc args = +let generate_conf_coq_config oc = section oc "Coq configuration."; let src_dirs = Coq_config.all_src_dirs in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; @@ -226,7 +218,7 @@ let generate_conf_coq_config oc args = ;; let generate_conf_files oc - { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; } + { v_files; mli_files; ml4_files; mlg_files; ml_files; mllib_files; mlpack_files; } = let module S = String in let map = map_sourced_list in @@ -235,6 +227,7 @@ let generate_conf_files oc fprintf oc "COQMF_MLIFILES = %s\n" (S.concat " " (map quote mli_files)); fprintf oc "COQMF_MLFILES = %s\n" (S.concat " " (map quote ml_files)); fprintf oc "COQMF_ML4FILES = %s\n" (S.concat " " (map quote ml4_files)); + fprintf oc "COQMF_MLGFILES = %s\n" (S.concat " " (map quote mlg_files)); fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files)); fprintf oc "COQMF_MLLIBFILES = %s\n" (S.concat " " (map quote mllib_files)); let cmdline_vfiles = filter_cmdline v_files in @@ -256,7 +249,7 @@ let rec logic_gcd acc = function let generate_conf_doc oc { defs; q_includes; r_includes } = let includes = List.map (forget_source > snd) (q_includes @ r_includes) in - let logpaths = List.map (CString.split '.') includes in + let logpaths = List.map (String.split_on_char '.') includes in let gcd = logic_gcd [] logpaths in let root = if gcd = [] then @@ -282,7 +275,7 @@ let generate_conf oc project args = fprintf oc "# %s\n\n" (String.concat " " (List.map quote args)); generate_conf_files oc project; generate_conf_includes oc project; - generate_conf_coq_config oc args; + generate_conf_coq_config oc; generate_conf_defs oc project; generate_conf_doc oc project; generate_conf_extra_target oc project.extra_targets; @@ -291,7 +284,7 @@ let generate_conf oc project args = let ensure_root_dir ({ ml_includes; r_includes; q_includes; - v_files; ml_files; mli_files; ml4_files; + v_files; ml_files; mli_files; ml4_files; mlg_files; mllib_files; mlpack_files } as project) = let exists f = List.exists (forget_source > f) in @@ -301,8 +294,8 @@ let ensure_root_dir || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes || (not_tops v_files && - not_tops mli_files && not_tops ml4_files && not_tops ml_files && - not_tops mllib_files && not_tops mlpack_files) + not_tops mli_files && not_tops ml4_files && not_tops mlg_files && + not_tops ml_files && not_tops mllib_files && not_tops mlpack_files) then project else @@ -386,8 +379,8 @@ let destination_of { ml_includes; q_includes; r_includes; } file = | _ -> assert false let share_prefix s1 s2 = - let s1 = CString.split '.' s1 in - let s2 = CString.split '.' s2 in + let s1 = String.split_on_char '.' s1 in + let s2 = String.split_on_char '.' s2 in match s1, s2 with | x :: _ , y :: _ -> x = y | _ -> false @@ -403,9 +396,10 @@ let _ = | "-destination-of" :: tgt :: rest -> Some tgt, rest | _ -> None, args in - let project = - try cmdline_args_to_project ~curdir:Filename.current_dir_name args - with Parsing_error s -> prerr_endline s; usage_coq_project () in + let project = + let warning_fn x = Format.eprintf "%s@\n%!" x in + try cmdline_args_to_project ~warning_fn ~curdir:Filename.current_dir_name args + with Parsing_error s -> prerr_endline s; usage_coq_makefile () in if only_destination <> None then begin destination_of project (Option.get only_destination); diff --git a/tools/coqc.ml b/tools/coqc.ml index 90d8e67c1e..ae841212a7 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 *) @@ -97,7 +97,7 @@ let parse_args () = |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-profile"|"-echo" |"-quiet" |"-silent"|"-m"|"-beautify"|"-strict-implicit" - |"-impredicative-set"|"-vm"|"-native-compiler" + |"-impredicative-set"|"-vm" |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" |"-stm-debug" @@ -109,9 +109,9 @@ let parse_args () = | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color" |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" - |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" + |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"|"-topfile" |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" - |"-o"|"-profile-ltac-cutoff"|"-mangle-names" + |"-o"|"-profile-ltac-cutoff"|"-mangle-names"|"-bytecode-compiler"|"-native-compiler" as o) :: rem -> begin match rem with @@ -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 12b5cab0ac..226a19678f 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -8,15 +8,24 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Printf +open Format open Coqdep_lexer open Coqdep_common -open System +open Minisys (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) are now in [Coqdep_common]. The code that remains here concerns the other options. Calling this complete coqdep with the [-boot] option should be equivalent to calling [coqdep_boot]. + + As of today, this module depends on the following Coq modules: + + - Flags + - Envars + - CoqProject_file + + All of it for `coqlib` handling. Ideally we would like to clean + coqlib handling up so this can be bootstrapped earlier. *) let option_D = ref false @@ -31,8 +40,7 @@ let warning_mult suf iter = let d' = Hashtbl.find tab f in if (Filename.dirname (file_name f d)) <> (Filename.dirname (file_name f d')) then begin - eprintf "*** Warning : the file %s is defined twice!\n" (f ^ suf); - flush stderr + coqdep_warning "the file %s is defined twice!" (f ^ suf) end with Not_found -> () end; Hashtbl.add tab f d @@ -80,9 +88,7 @@ let mL_dep_list b f = while true do let (Use_module str) = caml_action buf in if str = b then begin - eprintf "*** Warning : in file %s the" f; - eprintf " notation %s. is useless !\n" b; - flush stderr + coqdep_warning "in file %s the notation %s. is useless !\n" f b end else if not (List.mem str !deja_vu) then addQueue deja_vu str done; [] @@ -98,16 +104,13 @@ let affiche_Declare f dcl = printf "\n*** In file %s: \n" f; printf "Declare ML Module"; List.iter (fun str -> printf " \"%s\"" str) dcl; - printf ".\n"; - flush stdout + printf ".\n%!" let warning_Declare f dcl = - eprintf "*** Warning : in file %s, the ML modules" f; - eprintf " declaration should be\n"; + eprintf "*** Warning : in file %s, the ML modules declaration should be\n" f; eprintf "*** Declare ML Module"; List.iter (fun str -> eprintf " \"%s\"" str) dcl; - eprintf ".\n"; - flush stderr + eprintf ".\n%!" let traite_Declare f = let decl_list = ref ([] : string list) in @@ -149,7 +152,7 @@ let declare_dependencies () = List.iter (fun (name,_) -> traite_Declare (name^".v"); - flush stdout) + pp_print_flush std_formatter ()) (List.rev !vAccu) (** DAGs guaranteed to be transitive reductions *) @@ -426,11 +429,11 @@ let coq_dependencies_dump chan dumpboxes = (DAG.empty, List.fold_left (fun ih (file, _) -> insert_raw_graph file ih) [] !vAccu, List.map fst !vAccu) !vAccu in - fprintf chan "digraph dependencies {\n"; flush chan; + fprintf chan "digraph dependencies {\n"; if dumpboxes then print_graphs chan (pop_common_prefix graphs) else List.iter (fun (name, _) -> fprintf chan "\"%s\"[label=\"%s\"]\n" name (basename_noext name)) !vAccu; DAG.iter (fun name dep -> fprintf chan "\"%s\" -> \"%s\"\n" dep name) deps; - fprintf chan "}\n" + fprintf chan "}\n%!" end @@ -470,7 +473,8 @@ let add_r_include path l = add_rec_dir_import add_known path (split_period l) let treat_coqproject f = let open CoqProject_file in let iter_sourced f = List.iter (fun {thing} -> f thing) in - let project = read_project_file f in + let warning_fn x = coqdep_warning "%s" x in + let project = read_project_file ~warning_fn f in iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes; iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes; iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes; @@ -493,12 +497,12 @@ 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 () | "-slash" :: ll -> - Printf.eprintf "warning: option -slash has no effect and is deprecated.\n"; + coqdep_warning "warning: option -slash has no effect and is deprecated."; parse ll | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll @@ -509,6 +513,9 @@ let rec parse = function | f :: ll -> treat_file None f; parse ll | [] -> () +(* Exception to be raised by Envars *) +exception CoqlibError of string + let coqdep () = if Array.length Sys.argv < 2 then usage (); if not Coq_config.has_natdynlink then option_dynlink := No; @@ -520,18 +527,17 @@ let coqdep () = if !option_boot then begin add_rec_dir_import add_known "theories" ["Coq"]; add_rec_dir_import add_known "plugins" ["Coq"]; - add_caml_dir "tactics"; add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin - Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); + Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg)); let coqlib = Envars.coqlib () in add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user []; List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) - (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x))); + (Envars.xdg_dirs ~warn:(fun x -> coqdep_warning "%s" x)); List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; @@ -547,13 +553,13 @@ let coqdep () = | None -> () | Some (box, file) -> let chan = open_out file in - try Graph.coq_dependencies_dump chan box; close_out chan + let chan_fmt = formatter_of_out_channel chan in + try Graph.coq_dependencies_dump chan_fmt box; close_out chan with e -> close_out chan; raise e end let _ = try coqdep () - with CErrors.UserError(s,p) -> - let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in - Format.eprintf "%a@\n%!" Pp.pp_with pp + with CoqlibError msg -> + eprintf "*** Error: %s@\n%!" msg diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 70c983175d..713b2ad2b6 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -8,9 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Printf -open Coqdep_lexer +open Format open Unix +open Coqdep_lexer open Minisys (** [coqdep_boot] is a stripped-down version of [coqdep], whose @@ -20,14 +20,15 @@ open Minisys options (see for instance [option_dynlink] below). *) +let coqdep_warning args = + eprintf "*** Warning: @["; + kfprintf (fun fmt -> fprintf fmt "@]\n%!") err_formatter args + module StrSet = Set.Make(String) module StrList = struct type t = string list let compare = compare end module StrListMap = Map.Make(StrList) -let stderr = Pervasives.stderr -let stdout = Pervasives.stdout - type dynlink = Opt | Byte | Both | No | Variable let option_c = ref false @@ -40,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 @@ -102,10 +99,19 @@ let safe_hash_add cmp clq q (k, (v, b)) = For the ML files, the string is the basename without extension. *) +let same_path_opt s s' = + let nf s = (* ./foo/a.ml and foo/a.ml are the same file *) + if Filename.is_implicit s + then "." // s + else s + in + let s = match s with None -> "." | Some s -> nf s in + let s' = match s' with None -> "." | Some s' -> nf s' in + s = s' + let warning_ml_clash x s suff s' suff' = - if suff = suff' then - eprintf - "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff + if suff = suff' && not (same_path_opt s s') then + coqdep_warning "%s%s already found in %s (discarding %s%s)\n" x suff (match s with None -> "." | Some d -> d) ((match s' with None -> "." | Some d -> d) // x) suff @@ -170,13 +176,11 @@ let error_cannot_parse s (i,j) = exit 1 let warning_module_notfound f s = - eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!" + coqdep_warning "in file %s, library %s is required and has not been found in the loadpath!" f (String.concat "." s) let warning_declare f s = - eprintf "*** Warning: in file %s, declared ML module " f; - eprintf "%s has not been found!\n" s; - flush stderr + coqdep_warning "in file %s, declared ML module %s has not been found!" f s let warning_clash file dir = match StrListMap.find dir !clash_v with @@ -193,8 +197,7 @@ let warning_clash file dir = | _ -> assert false let warning_cannot_open_dir dir = - eprintf "*** Warning: cannot open %s\n" dir; - flush stderr + coqdep_warning "cannot open %s" dir let safe_assoc from verbose file k = if verbose && StrListMap.mem k !clash_v then warning_clash file k; @@ -441,15 +444,13 @@ let mL_dependencies () = in let efullname = escape fullname in printf "%s.cmo:%s%s\n" efullname dep intf; - printf "%s.cmx:%s%s\n" efullname dep_opt intf; - flush stdout) + printf "%s.cmx:%s%s\n%!" efullname dep_opt intf) (List.rev !mlAccu); List.iter (fun (name,dirname) -> let fullname = file_name name dirname in let (dep,_) = traite_fichier_ML fullname ".mli" in - printf "%s.cmi:%s\n" (escape fullname) dep; - flush stdout) + printf "%s.cmi:%s\n%!" (escape fullname) dep) (List.rev !mliAccu); List.iter (fun (name,dirname) -> @@ -458,8 +459,7 @@ let mL_dependencies () = let efullname = escape fullname in printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - flush stdout) + printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n%!" efullname efullname) (List.rev !mllibAccu); List.iter (fun (name,dirname) -> @@ -469,11 +469,11 @@ 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; - flush stdout) + printf "%!") (List.rev !mlpackAccu) let coq_dependencies () = @@ -486,8 +486,7 @@ let coq_dependencies () = printf "\n"; printf "%s.vio: %s.v" ename ename; traite_fichier_Coq ".vio" true (name ^ ".v"); - printf "\n"; - flush stdout) + printf "\n%!") (List.rev !vAccu) let rec suffixes = function @@ -497,9 +496,9 @@ let rec suffixes = function let add_caml_known phys_dir _ f = let basename,suff = - get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in + get_extension f [".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] in match suff with - | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff @@ -585,12 +584,12 @@ let rec treat_file old_dirname old_name = in Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> - (match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with + (match get_extension name [".v";".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] with | (base,".v") -> let name = file_name base dirname and absname = absolute_file_name base dirname in addQueue vAccu (name, absname) - | (base,(".ml"|".ml4" as ext)) -> addQueue mlAccu (base,ext,dirname) + | (base,(".ml"|".ml4"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname) | (base,".mli") -> addQueue mliAccu (base,dirname) | (base,".mllib") -> addQueue mllibAccu (base,dirname) | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index d0d7932435..91d2b45876 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -10,6 +10,8 @@ module StrSet : Set.S with type elt = string +val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a + (** [find_dir_logpath dir] Return the logical path of directory [dir] if it has been given one. Raise [Not_found] otherwise. In particular we can check if "." has been attributed a logical path 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 new file mode 100644 index 0000000000..9c0a6ccffe --- /dev/null +++ b/tools/coqdoc/dune @@ -0,0 +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 df493fdf7f..8d395b418f 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -77,7 +77,7 @@ let add_ref m loc m' sp id ty = let find m l = Hashtbl.find reftable (m, l) -let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) +let find_string s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) (* Coq modules *) @@ -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" @@ -185,7 +181,8 @@ let type_name = function let prepare_entry s = function | Notation -> (* We decode the encoding done in Dumpglob.cook_notation of coqtop *) - (* Encoded notations have the form section:sc:x_'++'_x where: *) + (* Encoded notations have the form section:entry:sc:x_'++'_x *) + (* where: *) (* - the section, if any, ends with a "." *) (* - the scope can be empty *) (* - tokens are separated with "_" *) @@ -202,10 +199,12 @@ let prepare_entry s = function let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in let h = try String.index_from s 0 ':' with _ -> err () in let i = try String.index_from s (h+1) ':' with _ -> err () in - let sc = String.sub s (h+1) (i-h-1) in - let ntn = Bytes.make (String.length s - i) ' ' in + let m = try String.index_from s (i+1) ':' with _ -> err () in + let entry = String.sub s (h+1) (i-h-1) in + let sc = String.sub s (i+1) (m-i-1) in + let ntn = Bytes.make (String.length s - m) ' ' in let k = ref 0 in - let j = ref (i+1) in + let j = ref (m+1) in let quoted = ref false in let l = String.length s - 1 in while !j <= l do @@ -227,7 +226,8 @@ let prepare_entry s = function incr j done; let ntn = Bytes.sub_string ntn 0 !k in - if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" + let ntn = if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" in + if entry = "" then ntn else entry ^ ":" ^ ntn | _ -> s diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 5cd301389b..7c9aad67fc 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -41,7 +41,7 @@ type index_entry = val find : coq_module -> loc -> index_entry (* Find what data is referred to by some string in some coq module *) -val find_string : coq_module -> string -> index_entry +val find_string : string -> index_entry val add_module : coq_module -> unit diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d252270021..606d954672 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 = @@ -76,7 +71,7 @@ let is_tactic = [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; - "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; + "info"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto"; "quote"; "eexact"; "autorewrite"; "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; @@ -431,7 +426,7 @@ module Latex = struct else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then try - let tag = Index.find_string (get_module false) s in + let tag = Index.find_string s in reference (translate s) tag with _ -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s @@ -706,7 +701,7 @@ module Html = struct else if is_keyword s then printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then - try reference (translate s) (Index.find_string (get_module false) s) + try reference (translate s) (Index.find_string s) with Not_found -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s @@ -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/coqworkmgr.ml b/tools/coqworkmgr.ml index 68aadcfccf..bfea141bb3 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -169,7 +169,7 @@ let main () = "-j",Arg.Set_int max_tokens, "max number of concurrent jobs"; "-d",Arg.Set debug, "do not detach (debug)"] in let usage = - "Prints on stdout an env variable assignement to be picked up by coq\n"^ + "Prints on stdout an env variable assignment to be picked up by coq\n"^ "instances in order to limit the maximum number of concurrent workers.\n"^ "The default value is 2.\n"^ "Usage:" in diff --git a/tools/dune b/tools/dune new file mode 100644 index 0000000000..31b70fb06c --- /dev/null +++ b/tools/dune @@ -0,0 +1,55 @@ +(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)) + +(executable + (name coqc) + (public_name coqc) + (package coq) + (modules coqc) + (libraries coq.toplevel)) + +(executable + (name coqworkmgr) + (public_name coqworkmgr) + (package coq) + (modules coqworkmgr) + (libraries coq.stm)) + +(executable + (name coqdep) + (public_name coqdep) + (package coq) + (modules coqdep_lexer coqdep_common coqdep) + (libraries coq.lib)) + +(ocamllex coqdep_lexer) + +(executable + (name coqwc) + (public_name coqwc) + (package coq) + (modules coqwc) + (libraries)) + +(ocamllex coqwc) + +(executables + (names coq_tex coq_dune) + (public_names coq-tex coq_dune) + (package coq) + (modules coq_tex coq_dune) + (libraries str)) diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml deleted file mode 100644 index d48c6d0af5..0000000000 --- a/tools/fake_ide.ml +++ /dev/null @@ -1,346 +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 [coqtop -ideslave] *) - -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 -ideslave.\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"; "-ideslave"] in - let coqtop_name = (* from ide/ideutils.ml *) - let prog_name = "fake_ide" in - let len_prog_name = String.length prog_name in - let fake_ide_path = Sys.executable_name in - let fake_ide_path_len = String.length fake_ide_path in - let pos = fake_ide_path_len - len_prog_name in - let rex = Str.regexp_string prog_name in - try - let i = Str.search_backward rex fake_ide_path pos in - String.sub fake_ide_path 0 i ^ "coqtop" ^ - String.sub fake_ide_path (i + len_prog_name) - (fake_ide_path_len - i - len_prog_name) - with Not_found -> assert false 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 coqtop_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/gallina-db.el b/tools/gallina-db.el deleted file mode 100644 index 9664f69f8b..0000000000 --- a/tools/gallina-db.el +++ /dev/null @@ -1,240 +0,0 @@ -;;; gallina-db.el --- coq keywords database utility functions -;; -;; Author: Pierre Courtieu <courtieu@lri.fr> -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; - -;;; We store all information on keywords (tactics or command) in big -;; tables (ex: `coq-tactics-db') From there we get: menus including -;; "smart" commands, completions for command coq-insert-... -;; abbrev tables and font-lock keyword - -;;; real value defined below - -;;; Commentary: -;; - -;;; Code: - -;(require 'proof-config) ; for proof-face-specs, a macro -;(require 'holes) - -(defconst coq-syntax-db nil - "Documentation-only variable, for coq keyword databases. -Each element of a keyword database contains the definition of a \"form\", of the -form: - -(MENUNAME ABBREV INSERT STATECH KWREG INSERT-FUN HIDE) - -MENUNAME is the name of form (or form variant) as it should appear in menus or -completion lists. - -ABBREV is the abbreviation for completion via \\[expand-abbrev]. - -INSERT is the complete text of the form, which may contain holes denoted by -\"#\" or \"@{xxx}\". - -If non-nil the optional STATECH specifies that the command is not state -preserving for coq. - -If non-nil the optional KWREG is the regexp to colorize correponding to the -keyword. ex: \"simple\\\\s-+destruct\" (\\\\s-+ meaning \"one or more spaces\"). -*WARNING*: A regexp longer than another one should be put FIRST. For example: - - (\"Module Type\" ... ... t \"Module\\s-+Type\") - (\"Module\" ... ... t \"Module\") - -Is ok because the longer regexp is recognized first. - -If non-nil the optional INSERT-FUN is the function to be called when inserting -the form (instead of inserting INSERT, except when using \\[expand-abbrev]). This -allows writing functions asking for more information to assist the user. - -If non-nil the optional HIDE specifies that this form should not appear in the -menu but only in interactive completions. - -Example of what could be in your emacs init file: - -(defvar coq-user-tactics-db - '( - (\"mytac\" \"mt\" \"mytac # #\" t \"mytac\") - (\"myassert by\" \"massb\" \"myassert ( # : # ) by #\" t \"assert\") - )) - -Explanation of the first line: the tactic menu entry mytac, abbreviated by mt, -will insert \"mytac # #\" where #s are holes to fill, and \"mytac\" becomes a -new keyword to colorize." ) - -(defun coq-insert-from-db (db prompt) - "Ask for a keyword, with completion on keyword database DB and insert. -Insert corresponding string with holes at point. If an insertion function is -present for the keyword, call it instead. see `coq-syntax-db' for DB -structure." - (let* ((tac (completing-read (concat prompt " (tab for completion) : ") - db nil nil)) - (infos (cddr (assoc tac db))) - (s (car infos)) ; completion to insert - (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function - (pt (point))) - (if f (funcall f) ; call f if present - (insert (or s tac)) ; insert completion and indent otherwise - (holes-replace-string-by-holes-backward-jump pt) - (indent-according-to-mode)))) - - - -(defun coq-build-regexp-list-from-db (db &optional filter) - "Take a keyword database DB and return the list of regexps for font-lock. -If non-nil Optional argument FILTER is a function applying to each line of DB. -For each line if FILTER returns nil, then the keyword is not added to the -regexp. See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l)) (tl (cdr l)) ; hd is the first infos list - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - ) - ;; TODO delete doublons - (when (and e5 (or (not filter) (funcall filter hd))) - (setq res (nconc res (list e5)))) ; careful: nconc destructive! - (setq l tl))) - res - )) - -;; Computes the max length of strings in a list -(defun max-length-db (db) - "Return the length of the longest first element (menu label) of DB. -See `coq-syntax-db' for DB structure." - (let ((l db) (res 0)) - (while l - (let ((lgth (length (car (car l))))) - (setq res (max lgth res)) - (setq l (cdr l)))) - res)) - - - -(defun coq-build-menu-from-db-internal (db lgth menuwidth) - "Take a keyword database DB and return one insertion submenu. -Argument LGTH is the max size of the submenu. Argument MENUWIDTH is the width -of the largest line in the menu (without abbrev and shortcut specifications). -Used by `coq-build-menu-from-db', which you should probably use instead. See -`coq-syntax-db' for DB structure." - (let ((l db) (res ()) (size lgth) - (keybind-abbrev (substitute-command-keys " \\[expand-abbrev]"))) - (while (and l (> size 0)) - (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - (e6 (car-safe tl5)) ; e6 = function for smart insertion - (e7 (car-safe (cdr-safe tl5))) ; e7 = if non-nil : hide in menu - (entry-with (max (- menuwidth (length e1)) 0)) - (spaces (make-string entry-with ? )) - ;;(restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth)) - ) - (when (not e7) ;; if not hidden - (let ((menu-entry - (vector - ;; menu entry label - (concat e1 (if (not e2) "" (concat spaces "(" e2 keybind-abbrev ")"))) - ;;insertion function if present otherwise insert completion - (if e6 e6 `(holes-insert-and-expand ,e3)) - t))) - (setq res (nconc res (list menu-entry)))));; append *in place* - (setq l tl) - (setq size (- size 1)))) - res)) - - -(defun coq-build-title-menu (db size) - "Build a title for the first submenu of DB, of size SIZE. -Return the string made of the first and the SIZE nth first element of DB, -separated by \"...\". Used by `coq-build-menu-from-db'. See `coq-syntax-db' -for DB structure." - (concat (car-safe (car-safe db)) - " ... " - (car-safe (car-safe (nthcdr (- size 1) db))))) - -(defun coq-sort-menu-entries (menu) - (sort menu - (lambda (x y) (string< - (downcase (elt x 0)) - (downcase (elt y 0)))))) - -(defun coq-build-menu-from-db (db &optional size) - "Take a keyword database DB and return a list of insertion menus for them. -Submenus contain SIZE entries (default 30). See `coq-syntax-db' for DB -structure." - ;; sort is destructive for the list, so copy list before sorting - (let* ((l (coq-sort-menu-entries (copy-list db))) (res ()) - (wdth (+ 2 (max-length-db db))) - (sz (or size 30)) (lgth (length l))) - (while l - (if (<= lgth sz) - (setq res ;; careful: nconc destructive! - (nconc res (list (cons - (coq-build-title-menu l lgth) - (coq-build-menu-from-db-internal l lgth wdth))))) - (setq res ; careful: nconc destructive! - (nconc res (list (cons - (coq-build-title-menu l sz) - (coq-build-menu-from-db-internal l sz wdth)))))) - (setq l (nthcdr sz l)) - (setq lgth (length l))) - res)) - -(defun coq-build-abbrev-table-from-db (db) - "Take a keyword database DB and return an abbrev table. -See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - ) - ;; careful: nconc destructive! - (when e2 - (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete))))) - (setq l tl))) - res)) - - -(defun filter-state-preserving (l) - ; checkdoc-params: (l) - "Not documented." - (not (nth 3 l))) ; fourth argument is nil --> state preserving command - -(defun filter-state-changing (l) - ; checkdoc-params: (l) - "Not documented." - (nth 3 l)) ; fourth argument is nil --> state preserving command - -(defconst coq-solve-tactics-face 'coq-solve-tactics-face - "Expression that evaluates to a face. -Required so that 'proof-solve-tactics-face is a proper facename") - - -;;A new face for tactics which fail when they don't kill the current goal -(defface coq-solve-tactics-face - '((t (:background "red"))) - "Face for names of closing tactics in proof scripts." - :group 'proof-faces) - - - - - -(provide 'gallina-db) - -;;; gallina-db.el ends here - -;** Local Variables: *** -;** fill-column: 80 *** -;** End: *** diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el deleted file mode 100644 index 7c59fb6ae8..0000000000 --- a/tools/gallina-syntax.el +++ /dev/null @@ -1,979 +0,0 @@ -;; gallina-syntax.el Font lock expressions for Coq -;; Copyright (C) 1997-2007 LFCS Edinburgh. -;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Maintainer: Pierre Courtieu <courtieu@lri.fr> - -;; gallina-syntax.el,v 9.9 2008/07/21 15:14:58 pier Exp - -;(require 'proof-syntax) -;(require 'proof-utils) ; proof-locate-executable -(require 'gallina-db) - - - - ;;; keyword databases - - -(defcustom coq-user-tactics-db nil - "User defined tactic information. See `coq-syntax-db' for - syntax. It is not necessary to add your own tactics here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your tactics will be colorized by font-lock - - 2 your tactics will be added to the menu and to completion when - calling \\[coq-insert-tactic] - - 3 you may define an abbreviation for your tactic." - - :type '(repeat sexp) - :group 'coq) - - -(defcustom coq-user-commands-db nil - "User defined command information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - -(defcustom coq-user-tacticals-db nil - "User defined tactical information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - -(defcustom coq-user-solve-tactics-db nil - "User defined closing tactics. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - - - -(defcustom coq-user-reserved-db nil - "User defined reserved keywords information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - - - -(defvar coq-tactics-db - (append - coq-user-tactics-db - '( - ("absurd " "abs" "absurd " t "absurd") - ("apply" "ap" "apply " t "apply") - ("assert by" "assb" "assert ( # : # ) by #" t "assert") - ("assert" "ass" "assert ( # : # )" t) - ;; ("assumption" "as" "assumption" t "assumption") - ("auto with arith" "awa" "auto with arith" t) - ("auto with" "aw" "auto with @{db}" t) - ("auto" "a" "auto" t "auto") - ("autorewrite with in using" "arwiu" "autorewrite with @{db,db...} in @{hyp} using @{tac}" t) - ("autorewrite with in" "arwi" "autorewrite with @{db,db...} in @{hyp}" t) - ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t) - ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite") - ("case" "c" "case " t "case") - ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv") - ("change in" "chi" "change # in #" t) - ("change with in" "chwi" "change # with # in #" t) - ("change with" "chw" "change # with" t) - ("change" "ch" "change " t "change") - ("clear" "cl" "clear" t "clear") - ("clearbody" "cl" "clearbody" t "clearbody") - ("cofix" "cof" "cofix" t "cofix") - ("coinduction" "coind" "coinduction" t "coinduction") - ("compare" "cmpa" "compare # #" t "compare") - ("compute" "cmpu" "compute" t "compute") - ;; ("congruence" "cong" "congruence" t "congruence") - ("constructor" "cons" "constructor" t "constructor") - ;; ("contradiction" "contr" "contradiction" t "contradiction") - ("cut" "cut" "cut" t "cut") - ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite") - ;; ("decide equality" "deg" "decide equality" t "decide\\s-+equality") - ("decompose record" "decr" "decompose record #" t "decompose\\s-+record") - ("decompose sum" "decs" "decompose sum #" t "decompose\\s-+sum") - ("decompose" "dec" "decompose [#] #" t "decompose") - ("dependent inversion" "depinv" "dependent inversion" t "dependent\\s-+inversion") - ("dependent inversion with" "depinvw" "dependent inversion # with #" t) - ("dependent inversion_clear" "depinvc" "dependent inversion_clear" t "dependent\\s-+inversion_clear") - ("dependent inversion_clear with" "depinvw" "dependent inversion_clear # with #" t) - ("dependent rewrite ->" "depr" "dependent rewrite -> @{id}" t "dependent\\s-+rewrite") - ("dependent rewrite <-" "depr<" "dependent rewrite <- @{id}" t) - ("destruct as" "desa" "destruct # as #" t) - ("destruct using" "desu" "destruct # using #" t) - ("destruct" "des" "destruct " t "destruct") - ;; ("discriminate" "dis" "discriminate" t "discriminate") - ("discrR" "discrR" "discrR" t "discrR") - ("double induction" "dind" "double induction # #" t "double\\s-+induction") - ("eapply" "eap" "eapply #" t "eapply") - ("eauto with arith" "eawa" "eauto with arith" t) - ("eauto with" "eaw" "eauto with @{db}" t) - ("eauto" "ea" "eauto" t "eauto") - ("econstructor" "econs" "econstructor" t "econstructor") - ("eexists" "eex" "eexists" t "eexists") - ("eleft" "eleft" "eleft" t "eleft") - ("elim using" "elu" "elim # using #" t) - ("elim" "e" "elim #" t "elim") - ("elimtype" "elt" "elimtype" "elimtype") - ("eright" "erig" "eright" "eright") - ("esplit" "esp" "esplit" t "esplit") - ;; ("exact" "exa" "exact" t "exact") - ("exists" "ex" "exists #" t "exists") - ;; ("fail" "fa" "fail" nil) - ;; ("field" "field" "field" t "field") - ("firstorder" "fsto" "firstorder" t "firstorder") - ("firstorder with" "fsto" "firstorder with #" t) - ("firstorder with using" "fsto" "firstorder # with #" t) - ("fold" "fold" "fold #" t "fold") - ;; ("fourier" "four" "fourier" t "fourier") - ("functional induction" "fi" "functional induction @{f} @{args}" t "functional\\s-+induction") - ("generalize dependent" "gd" "generalize dependent #" t "generalize\\s-+dependent") - ("generalize" "g" "generalize #" t "generalize") - ("hnf" "hnf" "hnf" t "hnf") - ("idtac" "id" "idtac" nil "idtac") ; also in tacticals with abbrev id - ("idtac \"" "id\"" "idtac \"#\"") ; also in tacticals - ("induction" "ind" "induction #" t "induction") - ("induction using" "indu" "induction # using #" t) - ("injection" "inj" "injection #" t "injection") - ("instantiate" "inst" "instantiate" t "instantiate") - ("intro" "i" "intro" t "intro") - ("intro after" "ia" "intro # after #" t) - ("intros" "is" "intros #" t "intros") - ("intros! (guess names)" nil "intros #" nil nil coq-insert-intros) - ("intros until" "isu" "intros until #" t) - ("intuition" "intu" "intuition #" t "intuition") - ("inversion" "inv" "inversion #" t "inversion") - ("inversion in" "invi" "inversion # in #" t) - ("inversion using" "invu" "inversion # using #" t) - ("inversion using in" "invui" "inversion # using # in #" t) - ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear") - ("lapply" "lap" "lapply" t "lapply") - ("lazy" "lazy" "lazy beta [#] delta iota zeta" t "lazy") - ("left" "left" "left" t "left") - ("linear" "lin" "linear" t "linear") - ("load" "load" "load" t "load") - ("move after" "mov" "move # after #" t "move") - ("omega" "o" "omega" t "omega") - ("pattern" "pat" "pattern" t "pattern") - ("pattern(s)" "pats" "pattern # , #" t) - ("pattern at" "pata" "pattern # at #" t) - ("pose" "po" "pose ( # := # )" t "pose") - ("prolog" "prol" "prolog" t "prolog") - ("quote" "quote" "quote" t "quote") - ("quote []" "quote2" "quote # [#]" t) - ("red" "red" "red" t "red") - ("refine" "ref" "refine" t "refine") - ;; ("reflexivity" "refl" "reflexivity #" t "reflexivity") - ("rename into" "ren" "rename # into #" t "rename") - ("replace with" "rep" "replace # with #" t "replace") - ("replace with in" "repi" "replace # with # in #" t) - ("rewrite <- in" "ri<" "rewrite <- # in #" t) - ("rewrite <-" "r<" "rewrite <- #" t) - ("rewrite in" "ri" "rewrite # in #" t) - ("rewrite" "r" "rewrite #" t "rewrite") - ("right" "rig" "right" t "right") - ;; ("ring" "ring" "ring #" t "ring") - ("set in * |-" "seth" "set ( # := #) in * |-" t) - ("set in *" "set*" "set ( # := #) in *" t) - ("set in |- *" "setg" "set ( # := #) in |- *" t) - ("set in" "seti" "set ( # := #) in #" t) - ("set" "set" "set ( # := #)" t "set") - ("setoid_replace with" "strep2" "setoid_replace # with #" t "setoid_replace") - ("setoid replace with" "strep" "setoid replace # with #" t "setoid\\s-+replace") - ("setoid_rewrite" "strew" "setoid_rewrite #" t "setoid_rewrite") - ("setoid rewrite" "strew" "setoid rewrite #" t "setoid\\s-+rewrite") - ("simpl" "s" "simpl" t "simpl") - ("simpl" "sa" "simpl # at #" t) - ("simple destruct" "sdes" "simple destruct" t "simple\\s-+destruct") - ("simple inversion" "sinv" "simple inversion" t "simple\\s-+inversion") - ("simple induction" "sind" "simple induction" t "simple\\s-+induction") - ("simplify_eq" "simeq" "simplify_eq @{hyp}" t "simplify_eq") - ("specialize" "spec" "specialize" t "specialize") - ("split" "sp" "split" t "split") - ("split_Rabs" "spra" "splitRabs" t "split_Rabs") - ("split_Rmult" "sprm" "splitRmult" t "split_Rmult") - ("stepl" "stl" "stepl #" t "stepl") - ("stepl by" "stlb" "stepl # by #" t) - ("stepr" "str" "stepr #" t "stepr") - ("stepr by" "strb" "stepr # by #" t) - ("subst" "su" "subst #" t "subst") - ("symmetry" "sy" "symmetry" t "symmetry") - ("symmetry in" "syi" "symmetry in #" t) - ;; ("tauto" "ta" "tauto" t "tauto") - ("transitivity" "trans" "transitivity #" t "transitivity") - ("trivial" "t" "trivial" t "trivial") - ("trivial with" "tw" "trivial with @{db}" t) - ("unfold" "u" "unfold #" t "unfold") - ("unfold(s)" "us" "unfold # , #" t) - ("unfold in" "unfi" "unfold # in #" t) - ("unfold at" "unfa" "unfold # at #" t) - )) - "Coq tactics information list. See `coq-syntax-db' for syntax. " - ) - -(defvar coq-solve-tactics-db - (append - coq-user-solve-tactics-db - '( - ("assumption" "as" "assumption" t "assumption") - ("by" "by" "by #" t "by") - ("congruence" "cong" "congruence" t "congruence") - ("contradiction" "contr" "contradiction" t "contradiction") - ("decide equality" "deg" "decide equality" t "decide\\s-+equality") - ("discriminate" "dis" "discriminate" t "discriminate") - ("exact" "exa" "exact" t "exact") - ("fourier" "four" "fourier" t "fourier") - ("fail" "fa" "fail" nil) - ("field" "field" "field" t "field") - ("omega" "o" "omega" t "omega") - ("reflexivity" "refl" "reflexivity #" t "reflexivity") - ("ring" "ring" "ring #" t "ring") - ("solve" nil "solve [ # | # ]" nil "solve") - ("tauto" "ta" "tauto" t "tauto") - )) - "Coq tactic(al)s that solve a subgoal." - ) - - -(defvar coq-tacticals-db - (append - coq-user-tacticals-db - '( - ("info" nil "info #" nil "info") - ("first" nil "first [ # | # ]" nil "first") - ("abstract" nil "abstract @{tac} using @{name}." nil "abstract") - ("do" nil "do @{num} @{tac}" nil "do") - ("idtac" nil "idtac") ; also in tactics - ; ("idtac \"" nil "idtac \"#\"") ; also in tactics - ("fail" "fa" "fail" nil "fail") - ; ("fail \"" "fa\"" "fail" nil) ; - ; ("orelse" nil "orelse #" t "orelse") - ("repeat" nil "repeat #" nil "repeat") - ("try" nil "try #" nil "try") - ("progress" nil "progress #" nil "progress") - ("|" nil "[ # | # ]" nil) - ("||" nil "# || #" nil) - )) - "Coq tacticals information list. See `coq-syntax-db' for syntax.") - - - - -(defvar coq-decl-db - '( - ("Axiom" "ax" "Axiom # : #" t "Axiom") - ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors") - ("Hint Extern" "he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." t "Hint\\s-+Extern") - ("Hint Immediate" "hi" "Hint Immediate # : @{db}." t "Hint\\s-+Immediate") - ("Hint Resolve" "hr" "Hint Resolve # : @{db}." t "Hint\\s-+Resolve") - ("Hint Rewrite ->" "hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." t "Hint\\s-+Rewrite") - ("Hint Rewrite <-" "hrw" "Hint Rewrite <- @{t1,t2...} using @{tac} : @{db}." t ) - ("Hint Unfold" "hu" "Hint Unfold # : #." t "Hint\\s-+Unfold") - ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis") - ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses") - ("Parameter" "par" "Parameter #: #" t "Parameter") - ("Parameters" "par" "Parameter #: #" t "Parameters") - ("Conjecture" "conj" "Conjecture #: #." t "Conjecture") - ("Variable" "v" "Variable #: #." t "Variable") - ("Variables" "vs" "Variables # , #: #." t "Variables") - ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") - ) - "Coq declaration keywords information list. See `coq-syntax-db' for syntax." - ) - -(defvar coq-defn-db - '( - ("CoFixpoint" "cfix" "CoFixpoint # (#:#) : # :=\n#." t "CoFixpoint") - ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive") - ("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module") - ("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful - ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t) - ("Declare Module Import <: :=" "dmi2" "Declare Module # <: # := #." t);; careful - ("Declare Module Export : :=" "dme" "Declare Module # : # := #." t) - ("Declare Module Export <: :=" "dme2" "Declare Module # <: # := #." t);; careful - ("Definition" "def" "Definition #:# := #." t "Definition");; careful - ("Definition (2 args)" "def2" "Definition # (# : #) (# : #):# := #." t) - ("Definition (3 args)" "def3" "Definition # (# : #) (# : #) (# : #):# := #." t) - ("Definition (4 args)" "def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) - ("Program Definition" "pdef" "Program Definition #:# := #." t "Program\\s-+Definition");; careful ? - ("Program Definition (2 args)" "pdef2" "Program Definition # (# : #) (# : #):# := #." t) - ("Program Definition (3 args)" "pdef3" "Program Definition # (# : #) (# : #) (# : #):# := #." t) - ("Program Definition (4 args)" "pdef4" "Program Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) - ("Derive Inversion" nil "Derive Inversion @{id} with # Sort #." t "Derive\\s-+Inversion") - ("Derive Dependent Inversion" nil "Derive Dependent Inversion @{id} with # Sort #." t "Derive\\s-+Dependent\\s-+Inversion") - ("Derive Inversion_clear" nil "Derive Inversion_clear @{id} with # Sort #." t) - ("Fixpoint" "fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Fixpoint") - ("Program Fixpoint" "pfix" "Program Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Program\\s-+Fixpoint") - ("Program Fixpoint measure" "pfixm" "Program Fixpoint # (#:#) {measure @{arg} @{f}} : # :=\n#." t) - ("Program Fixpoint wf" "pfixwf" "Program Fixpoint # (#:#) {wf @{arg} @{f}} : # :=\n#." t) - ("Function" "func" "Function # (#:#) {struct @{arg}} : # :=\n#." t "Function") - ("Function measure" "funcm" "Function # (#:#) {measure @{f} @{arg}} : # :=\n#." t) - ("Function wf" "func wf" "Function # (#:#) {wf @{R} @{arg}} : # :=\n#." t) - ("Functional Scheme with" "fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." t ) - ("Functional Scheme" "fs" "Functional Scheme @{name} := Induction for @{fun}." t "Functional\\s-+Scheme") - ("Inductive" "indv" "Inductive # : # := # : #." t "Inductive") - ("Inductive (2 args)" "indv2" "Inductive # : # :=\n| # : #\n| # : #." t ) - ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t ) - ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Variant" "indv" "Variant # : # := # : #." t "Variant") - ("Variant (2 args)" "indv2" "Variant # : # :=\n| # : #\n| # : #." t ) - ("Variant (3 args)" "indv3" "Variant # : # :=\n| # : #\n| # : #\n| # : #." t ) - ("Variant (4 args)" "indv4" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Variant (5 args)" "indv5" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Let" "Let" "Let # : # := #." t "Let") - ("Ltac" "ltac" "Ltac # := #" t "Ltac") - ("Module :=" "mo" "Module # : # := #." t ) ; careful - ("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful - ("Module Import :=" "moi" "Module Import # : # := #." t ) ; careful - ("Module Import <: :=" "moi2" "Module Import # <: # := #." t ) ; careful - ("Module Export :=" "moe" "Module Export # : # := #." t ) ; careful - ("Module Export <: :=" "moe2" "Module Export# <: # := #." t ) ; careful - ("Record" "rec" "Record # : # := {\n# : #;\n# : # }" t "Record") - ("Scheme" "sc" "Scheme @{name} := #." t "Scheme") - ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t) - ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t) - ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure") - ) - "Coq definition keywords information list. See `coq-syntax-db' for syntax. " - ) - -;; modules and section are indented like goal starters -(defvar coq-goal-starters-db - '( - ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism") - ("Chapter" "chp" "Chapter # : #." t "Chapter") - ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") - ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) - ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) - ("Definition goal" "defg" "Definition #:#.\n#\nQed." t);; careful - ("Fact" "fct" "Fact # : #." t "Fact") - ("Goal" nil "Goal #." t "Goal") - ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") - ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma") - ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module) - ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful - ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful - ("Module <:" "moi2" "Module # <: #.\n#\nEnd #." t ) ; careful - ("Remark" "rk" "Remark # : #.\n#\nQed." t "Remark") - ("Section" "sec" "Section #." t "Section") - ("Theorem" "th" "Theorem # : #.\n#\nQed." t "Theorem") - ("Program Theorem" "pth" "Program Theorem # : #.\nProof.\n#\nQed." t "Program\\s-+Theorem") - ("Obligation" "obl" "Obligation #.\n#\nQed." t "Obligation") - ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation") - ) - "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " - ) - -;; command that are not declarations, definition or goal starters -(defvar coq-other-commands-db - '( - ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu - ("About" nil "About #." nil "About") - ("Add" nil "Add #." nil "Add" nil t) - ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring") - ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring") - ("Add Field" nil "Add Field #." t "Add\\s-+Field") - ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath") - ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") - ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism") - ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") - ("Add Printing Constructor" nil "Add Printing Constructor #." t "Add\\s-+Printing\\s-+Constructor") - ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") - ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") - ("Add Printing Record" nil "Add Printing Record #." t "Add\\s-+Printing\\s-+Record") - ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") - ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") - ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") - ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") - ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") - ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") - ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") - ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") - ("Cd" nil "Cd #." nil "Cd") - ("Check" nil "Check" nil "Check") - ("Close Local Scope" "cllsc" "Close Local Scope #" t "Close\\s-+Local\\s-+Scope") - ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") - ("Comments" nil "Comments #." nil "Comments") - ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) - ("Eval" nil "Eval #." nil "Eval") - ("Export" nil "Export #." t "Export") - ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant") - ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant") - ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract") - ("Extraction" "extr" "Extraction @{id}." nil "Extraction") - ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil) - ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline") - ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline") - ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language") - ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library") - ("Focus" nil "Focus #." nil "Focus") - ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion") - ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off") - ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On") - ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") - ("Import" nil "Import #." t "Import") - ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") - ("Inspect" nil "Inspect #." nil "Inspect") - ("Locate" nil "Locate" nil "Locate") - ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File") - ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library") - ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) - ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) - ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) - ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t) - ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t) - ("Notation Local (only parsing)" "notslp" "Notation Local # := # (only parsing)." t) - ("Notation Local" "notsl" "Notation Local # := #." t "Notation\\s-+Local") - ("Notation (simple)" "nots" "Notation # := #." t "Notation") - ("Opaque" nil "Opaque #." nil "Opaque") - ("Obligations Tactic" nil "Obligations Tactic := #." t "Obligations\\s-+Tactic") - ("Open Local Scope" "oplsc" "Open Local Scope #" t "Open\\s-+Local\\s-+Scope") - ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope") - ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions") - ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint) - ("Print" "p" "Print #." nil "Print") - ("Qed" nil "Qed." nil "Qed") - ("Pwd" nil "Pwd." nil "Pwd") - ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction") - ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library") - ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If") - ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let") - ("Require Export" nil "Require Export #." t "Require\\s-+Export") - ("Require Import" nil "Require Import #." t "Require\\s-+Import") - ("Require" nil "Require #." t "Require") - ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") - ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") - ("Search" nil "Search #" nil "Search") - ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") - ("SearchPattern" nil "SearchPattern #" nil "SearchPattern") - ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") - ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline") - ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize") - ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments") - ("Set Strict Implicit" nil "Set Strict Implicit" t "Set\\s-+Strict\\s-+Implicit") - ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth") - ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard") - ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All") - ("Set Printing Records" nil "Set Printing Records" t "Set\\s-+Printing\\s-+Records") - ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit") - ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions") - ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") - ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo") - ("Show" nil "Show #." nil "Show") - ("Solve Obligations" "oblssolve" "Solve Obligations using #." nil "Solve\\s-+Obligations") - ("Test" nil "Test" nil "Test" nil t) - ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") - ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") - ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let") - ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth") - ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width") - ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard") - ("Transparent" nil "Transparent #." nil "Transparent") - ("Unfocus" nil "Unfocus." nil "Unfocus") - ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline") - ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize") - ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset\\s-+Implicit\\s-+Arguments") - ("Unset Strict Implicit" nil "Unset Strict Implicit" t "Unset\\s-+Strict\\s-+Implicit") - ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset\\s-+Printing\\s-+Synth") - ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset\\s-+Printing\\s-+Wildcard") - ("Unset Hyps Limit" nil "Unset Hyps Limit" nil "Unset\\s-+Hyps\\s-+Limit") - ("Unset Printing All" "unsprall" "Unset Printing All" nil "Unset\\s-+Printing\\s-+All") - ("Unset Printing Coercion" nil "Unset Printing Coercion #." t "Unset\\s-+Printing\\s-+Coercion") - ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions") - ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations") - ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo") - ; ("print" "pr" "print #" "print") - ) - "Command that are not declarations, definition or goal starters." - ) - -(defvar coq-commands-db - (append coq-decl-db coq-defn-db coq-goal-starters-db - coq-other-commands-db coq-user-commands-db) - "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " - ) - - -(defvar coq-terms-db - '( - ("fun (1 args)" "f" "fun #:# => #" nil "fun") - ("fun (2 args)" "f2" "fun (#:#) (#:#) => #") - ("fun (3 args)" "f3" "fun (#:#) (#:#) (#:#) => #") - ("fun (4 args)" "f4" "fun (#:#) (#:#) (#:#) (#:#) => #") - ("forall" "fo" "forall #:#,#" nil "forall") - ("forall (2 args)" "fo2" "forall (#:#) (#:#), #") - ("forall (3 args)" "fo3" "forall (#:#) (#:#) (#:#), #") - ("forall (4 args)" "fo4" "forall (#:#) (#:#) (#:#) (#:#), #") - ("if" "if" "if # then # else #" nil "if") - ("let in" "li" "let # := # in #" nil "let") - ("match! (from type)" nil "" nil "match" coq-insert-match) - ("match with" "m" "match # with\n| # => #\nend") - ("match with 2" "m2" "match # with\n| # => #\n| # => #\nend") - ("match with 3" "m3" "match # with\n| # => #\n| # => #\n| # => #\nend") - ("match with 4" "m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend") - ("match with 5" "m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend") - ) - "Coq terms keywords information list. See `coq-syntax-db' for syntax. " - ) - - - - - - - - ;;; Goals (and module/sections) starters detection - - -;; ----- keywords for font-lock. - -;; FIXME da: this one function breaks the nice configuration of Proof General: -;; would like to have proof-goal-regexp instead. -;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, -;; so it appears more difficult than just a proof-goal-regexp setting. -;; Future improvement may simply to be allow a function value for -;; proof-goal-regexp. - -;; FIXME Pierre: the right way IMHO here would be to set a span -;; property 'goalcommand when coq prompt says it (if the name of -;; current proof has changed). - -;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry -;; for the french: -;;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de -;; module (donc pas de Definition truc:machin. Lemma, Theorem ... ) -;; -;; *) la commande Module M [ ( : | <: ) MTYP ] [ := MEXPR ] est valable -;; uniquement hors d'un MT -;; - si :=MEXPR est absent, elle demarre un nouveau module interactif -;; - si :=MEXPR est present, elle definit un module -;; (la fonction vernac_define_module dans toplevel/vernacentries) -;; -;; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ] -;; est valable uniquement dans un MT -;; - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module -;; interactif -;; - si (:=MEXPR absent, :MTYP present) -;; ou (:=MEXPR present, :MTYP absent) -;; elle declare un module. -;; (la fonction vernac_declare_module dans toplevel/vernacentries) - -(defun coq-count-match (regexp strg) - "Count the number of (maximum, non overlapping) matching substring - of STRG matching REGEXP. Empty match are counted once." - (let ((nbmatch 0) (str strg)) - (while (and (proof-string-match regexp str) (not (string-equal str ""))) - (incf nbmatch) - (if (= (match-end 0) 0) (setq str (substring str 1)) - (setq str (substring str (match-end 0))))) - nbmatch)) - -;; This function is used for amalgamating a proof into a single -;; goal-save region (proof-goal-command-p used in -;; proof-done-advancing-save in generic/proof-script.el) for coq < -;; 8.0. It is the test when looking backward the start of the proof. -;; It is NOT used for coq > v8.1 -;; (coq-find-and-forget in gallina.el uses state numbers, proof numbers and -;; lemma names given in the prompt) - -;; compatibility with v8.0, will delete it some day -(defun coq-goal-command-str-v80-p (str) - "See `coq-goal-command-p'." - (let* ((match (coq-count-match "\\<match\\>" str)) - (with (coq-count-match "\\<with\\>" str)) - (letwith (+ (coq-count-match "\\<let\\>" str) (- with match))) - (affect (coq-count-match ":=" str))) - - (and (proof-string-match coq-goal-command-regexp str) - (not ; - (and - (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str) - (not (= letwith affect)))) - (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) - ) - ) - ) - -;; Module and or section openings are detected syntactically. Module -;; *openings* are difficult to detect because there can be Module -;; ...with X := ... . So we need to count :='s to detect real openings. - -;; TODO: have opened section/chapter in the prompt too, and get rid of -;; syntactical tests everywhere -(defun coq-module-opening-p (str) - "Decide whether STR is a module or section opening or not. -Used by `coq-goal-command-p'" - (let* ((match (coq-count-match "\\<match\\>" str)) - (with (coq-count-match "\\<with\\>" str)) - (letwith (+ (coq-count-match "\\<let\\>" str) (- with match))) - (affect (coq-count-match ":=" str))) - (and (proof-string-match "\\`\\(Module\\)\\>" str) - (= letwith affect)) - )) - -(defun coq-section-command-p (str) - (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str)) - - -(defun coq-goal-command-str-v81-p (str) - "Decide syntactically whether STR is a goal start or not. Use - `coq-goal-command-p-v81' on a span instead if possible." - (coq-goal-command-str-v80-p str) - ) - -;; This is the function that tests if a SPAN is a goal start. All it -;; has to do is look at the 'goalcmd attribute of the span. -;; It also looks if this is not a module start. - -;; TODO: have also attributes 'modulecmd and 'sectioncmd. This needs -;; something in the coq prompt telling the name of all opened modules -;; (like for open goals), and use it to set goalcmd --> no more need -;; to look at Modules and section (actually indentation will still -;; need it) -(defun coq-goal-command-p-v81 (span) - "see `coq-goal-command-p'" - (or (span-property span 'goalcmd) - ;; module and section starts are detected here - (let ((str (or (span-property span 'cmd) ""))) - (or (coq-section-command-p str) - (coq-module-opening-p str)) - ))) - -;; In coq > 8.1 This is used only for indentation. -(defun coq-goal-command-str-p (str) - "Decide whether argument is a goal or not. Use - `coq-goal-command-p' on a span instead if posible." - (cond - (coq-version-is-V8-1 (coq-goal-command-str-v81-p str)) - (coq-version-is-V8-0 (coq-goal-command-str-v80-p str)) - (t (coq-goal-command-str-v80-p str));; this is temporary - )) - -;; This is used for backtracking -(defun coq-goal-command-p (span) - "Decide whether argument is a goal or not." - (cond - (coq-version-is-V8-1 (coq-goal-command-p-v81 span)) - (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd))) - (t (coq-goal-command-str-v80-p (span-property span 'cmd)));; this is temporary - )) - -(defvar coq-keywords-save-strict - '("Defined" - "Qed" - "End" - "Admitted" - "Abort" - )) - -(defvar coq-keywords-save - (append coq-keywords-save-strict '("Proof")) - ) - -(defun coq-save-command-p (span str) - "Decide whether argument is a Save command or not" - (or (proof-string-match coq-save-command-regexp-strict str) - (and (proof-string-match "\\`Proof\\>" str) - (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str))) - ) - ) - - -(defvar coq-keywords-kill-goal - '("Abort")) - -;; Following regexps are all state changing -(defvar coq-keywords-state-changing-misc-commands - (coq-build-regexp-list-from-db coq-commands-db 'filter-state-changing)) - -(defvar coq-keywords-goal - (coq-build-regexp-list-from-db coq-goal-starters-db)) - -(defvar coq-keywords-decl - (coq-build-regexp-list-from-db coq-decl-db)) - -(defvar coq-keywords-defn - (coq-build-regexp-list-from-db coq-defn-db)) - - -(defvar coq-keywords-state-changing-commands - (append - coq-keywords-state-changing-misc-commands - coq-keywords-decl ; all state changing - coq-keywords-defn ; idem - coq-keywords-goal)) ; idem - - -;; -(defvar coq-keywords-state-preserving-commands - (coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving)) - -;; concat this is faster that redoing coq-build-regexp-list-from-db on -;; whole commands-db -(defvar coq-keywords-commands - (append coq-keywords-state-changing-commands - coq-keywords-state-preserving-commands) - "All commands keyword.") - -(defvar coq-solve-tactics - (coq-build-regexp-list-from-db coq-solve-tactics-db) - "Keywords for closing tactic(al)s.") - -(defvar coq-tacticals - (coq-build-regexp-list-from-db coq-tacticals-db) - "Keywords for tacticals in a Coq script.") - - - ;; From JF Monin: -(defvar coq-reserved - (append - coq-user-reserved-db - '( - "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match" - "return" "struct" "else" "end" "if" "in" "into" "let" "then" - "using" "with" "beta" "delta" "iota" "zeta" "after" "until" - "at" "Sort" "Time")) - "Reserved keywords of Coq.") - - -(defvar coq-state-changing-tactics - (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) - -(defvar coq-state-preserving-tactics - (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-preserving)) - - -(defvar coq-tactics - (append coq-state-changing-tactics coq-state-preserving-tactics)) - -(defvar coq-retractable-instruct - (append coq-state-changing-tactics coq-keywords-state-changing-commands)) - -(defvar coq-non-retractable-instruct - (append coq-state-preserving-tactics - coq-keywords-state-preserving-commands)) - -(defvar coq-keywords - (append coq-keywords-goal coq-keywords-save coq-keywords-decl - coq-keywords-defn coq-keywords-commands) - "All keywords in a Coq script.") - - - -(defvar coq-symbols - '("|" - "||" - ":" - ";" - "," - "(" - ")" - "[" - "]" - "{" - "}" - ":=" - "=>" - "->" - ".") - "Punctuation Symbols used by Coq.") - -;; ----- regular expressions -(defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" - "A regexp indicating that the Coq process has identified an error.") - -(defvar coq-id proof-id) -(defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)") - -(defvar coq-ids (proof-ids coq-id " ")) - -(defun coq-first-abstr-regexp (paren end) - (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) - -(defcustom coq-variable-highlight-enable t - "Activates partial bound variable highlighting" - :type 'boolean - :group 'coq) - - -(defvar coq-font-lock-terms - (if coq-variable-highlight-enable - (list - ;; lambda binders - (list (coq-first-abstr-regexp "\\<fun\\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face) - ;; forall binder - (list (coq-first-abstr-regexp "\\<forall\\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) - ; (list "\\<forall\\>" - ; (list 0 font-lock-type-face) - ; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil - ; (list 0 font-lock-variable-name-face))) - ;; parenthesized binders - (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) - )) - "*Font-lock table for Coq terms.") - - - -;; According to Coq, "Definition" is both a declaration and a goal. -;; It is understood here as being a goal. This is important for -;; recognizing global identifiers, see coq-global-p. -(defconst coq-save-command-regexp-strict - (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)"))) -(defconst coq-save-command-regexp - (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save) - "\\)"))) -(defconst coq-save-with-hole-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) - -(defconst coq-goal-command-regexp - (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal))) - -(defconst coq-goal-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-goal) - "\\)\\s-+\\(" coq-id "\\)\\s-*:?")) - -(defconst coq-decl-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-decl) - "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) - -;; (defconst coq-decl-with-hole-regexp -;; (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil)) - -(defconst coq-defn-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) - "\\)\\s-+\\(" coq-id "\\)")) - -;; must match: -;; "with f x y :" (followed by = or not) -;; "with f x y (z:" (not followed by =) -;; BUT NOT: -;; "with f ... (x:=" -;; "match ... with .. => " -(defconst coq-with-with-hole-regexp - (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*" - coq-id "\\s-*:[^=]\\)")) -;; marche aussi a peu pres -;; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) -;;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" -(defvar coq-font-lock-keywords-1 - (append - coq-font-lock-terms - (list - (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) - (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) - (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) - (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face) - (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) - (cons (proof-ids-to-regexp (list "Set" "Type" "Prop")) 'font-lock-type-face) - (cons "============================" 'font-lock-keyword-face) - (cons "Subtree proved!" 'font-lock-keyword-face) - (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face) - (list "^\\([^ \n]+\\) \\(is defined\\)" - (list 2 'font-lock-keyword-face t) - (list 1 'font-lock-function-name-face t)) - - (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)) - (if coq-variable-highlight-enable (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face))) - (list - (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-with-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-save-with-hole-regexp 2 'font-lock-function-name-face) - ;; Remove spurious variable and function faces on commas. - '(proof-zap-commas)))) - -(defvar coq-font-lock-keywords coq-font-lock-keywords-1) - -(defun coq-init-syntax-table () - "Set appropriate values for syntax table in current buffer." - - (modify-syntax-entry ?\$ ".") - (modify-syntax-entry ?\/ ".") - (modify-syntax-entry ?\\ ".") - (modify-syntax-entry ?+ ".") - (modify-syntax-entry ?- ".") - (modify-syntax-entry ?= ".") - (modify-syntax-entry ?% ".") - (modify-syntax-entry ?< ".") - (modify-syntax-entry ?> ".") - (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "_") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?\| ".") - -;; should maybe be "_" but it makes coq-find-and-forget (in gallina.el) bug - (modify-syntax-entry ?\. ".") - - (condition-case nil - ;; Try to use Emacs-21's nested comments. - (modify-syntax-entry ?\* ". 23n") - ;; Revert to non-nested comments if that failed. - (error (modify-syntax-entry ?\* ". 23"))) - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) - - -(defconst coq-generic-expression - (mapcar (lambda (kw) - (list (capitalize kw) - (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" ) - 1)) - (append coq-keywords-decl coq-keywords-defn coq-keywords-goal))) - -(provide 'gallina-syntax) - ;;; gallina-syntax.el ends here - -; Local Variables: *** -; indent-tabs-mode: nil *** -; End: *** diff --git a/tools/gallina.el b/tools/gallina.el deleted file mode 100644 index cbc13118a6..0000000000 --- a/tools/gallina.el +++ /dev/null @@ -1,142 +0,0 @@ -;; gallina.el --- Coq mode editing commands for Emacs -;; -;; Jean-Christophe Filliatre, march 1995 -;; Shamelessly copied from caml.el, Xavier Leroy, july 1993. -;; -;; modified by Marco Maggesi <maggesi@math.unifi.it> for gallina-inferior - -; compatibility code for proofgeneral files -(require 'coq-font-lock) -; ProofGeneral files. remember to remove coq version tests in -; gallina-syntax.el -(require 'gallina-syntax) - -(defvar coq-mode-map nil - "Keymap used in Coq mode.") -(if coq-mode-map - () - (setq coq-mode-map (make-sparse-keymap)) - (define-key coq-mode-map "\t" 'coq-indent-command) - (define-key coq-mode-map "\M-\t" 'coq-unindent-command) - (define-key coq-mode-map "\C-c\C-c" 'compile) -) - -(defvar coq-mode-syntax-table nil - "Syntax table in use in Coq mode buffers.") -(if coq-mode-syntax-table - () - (setq coq-mode-syntax-table (make-syntax-table)) - ; ( is first character of comment start - (modify-syntax-entry ?\( "()1" coq-mode-syntax-table) - ; * is second character of comment start, - ; and first character of comment end - (modify-syntax-entry ?* ". 23" coq-mode-syntax-table) - ; ) is last character of comment end - (modify-syntax-entry ?\) ")(4" coq-mode-syntax-table) - ; quote is a string-like delimiter (for character literals) - (modify-syntax-entry ?' "\"" coq-mode-syntax-table) - ; quote is part of words - (modify-syntax-entry ?' "w" coq-mode-syntax-table) -) - -(defvar coq-mode-indentation 2 - "*Indentation for each extra tab in Coq mode.") - -(defun coq-mode-variables () - (set-syntax-table coq-mode-syntax-table) - (make-local-variable 'paragraph-start) - (setq paragraph-start (concat "^$\\|" page-delimiter)) - (make-local-variable 'paragraph-separate) - (setq paragraph-separate paragraph-start) - (make-local-variable 'paragraph-ignore-fill-prefix) - (setq paragraph-ignore-fill-prefix t) - (make-local-variable 'require-final-newline) - (setq require-final-newline t) - (make-local-variable 'comment-start) - (setq comment-start "(* ") - (make-local-variable 'comment-end) - (setq comment-end " *)") - (make-local-variable 'comment-column) - (setq comment-column 40) - (make-local-variable 'comment-start-skip) - (setq comment-start-skip "(\\*+ *") - (make-local-variable 'parse-sexp-ignore-comments) - (setq parse-sexp-ignore-comments nil) - (make-local-variable 'indent-line-function) - (setq indent-line-function 'coq-indent-command) - (make-local-variable 'font-lock-keywords) - (setq font-lock-defaults '(coq-font-lock-keywords-1))) - -;;; The major mode - -(defun coq-mode () - "Major mode for editing Coq code. -Tab at the beginning of a line indents this line like the line above. -Extra tabs increase the indentation level. -\\{coq-mode-map} -The variable coq-mode-indentation indicates how many spaces are -inserted for each indentation level." - (interactive) - (kill-all-local-variables) - (setq major-mode 'coq-mode) - (setq mode-name "coq") - (use-local-map coq-mode-map) - (coq-mode-variables) - (run-hooks 'coq-mode-hook)) - -;;; Indentation stuff - -(defun coq-in-indentation () - "Tests whether all characters between beginning of line and point -are blanks." - (save-excursion - (skip-chars-backward " \t") - (bolp))) - -(defun coq-indent-command () - "Indent the current line in Coq mode. -When the point is at the beginning of an empty line, indent this line like -the line above. -When the point is at the beginning of an indented line -\(i.e. all characters between beginning of line and point are blanks\), -increase the indentation by one level. -The indentation size is given by the variable coq-mode-indentation. -In all other cases, insert a tabulation (using insert-tab)." - (interactive) - (let* ((begline - (save-excursion - (beginning-of-line) - (point))) - (current-offset - (- (point) begline)) - (previous-indentation - (save-excursion - (if (eq (forward-line -1) 0) (current-indentation) 0)))) - (cond ((and (bolp) - (looking-at "[ \t]*$") - (> previous-indentation 0)) - (indent-to previous-indentation)) - ((coq-in-indentation) - (indent-to (+ current-offset coq-mode-indentation))) - (t - (insert-tab))))) - -(defun coq-unindent-command () - "Decrease indentation by one level in Coq mode. -Works only if the point is at the beginning of an indented line -\(i.e. all characters between beginning of line and point are blanks\). -Does nothing otherwise." - (interactive) - (let* ((begline - (save-excursion - (beginning-of-line) - (point))) - (current-offset - (- (point) begline))) - (if (and (>= current-offset coq-mode-indentation) - (coq-in-indentation)) - (backward-delete-char-untabify coq-mode-indentation)))) - -;;; gallina.el ends here - -(provide 'gallina) diff --git a/tools/gallina.ml b/tools/gallina.ml deleted file mode 100644 index c7ff76becd..0000000000 --- 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 1a594aebbf..0000000000 --- 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 } diff --git a/tools/inferior-coq.el b/tools/inferior-coq.el deleted file mode 100644 index b79d97d66e..0000000000 --- a/tools/inferior-coq.el +++ /dev/null @@ -1,324 +0,0 @@ -;;; inferior-coq.el --- Run an inferior Coq process. -;;; -;;; Copyright (C) Marco Maggesi <maggesi@math.unifi.it> -;;; Time-stamp: "2002-02-28 12:15:04 maggesi" - - -;; Emacs Lisp Archive Entry -;; Filename: inferior-coq.el -;; Version: 1.0 -;; Keywords: process coq -;; Author: Marco Maggesi <maggesi@math.unifi.it> -;; Maintainer: Marco Maggesi <maggesi@math.unifi.it> -;; Description: Run an inferior Coq process. -;; URL: http://www.math.unifi.it/~maggesi/ -;; Compatibility: Emacs20, Emacs21, XEmacs21 - -;; This is free software; you can redistribute it and/or modify it under -;; the terms of the GNU General Public License as published by the Free -;; Software Foundation; either version 2, or (at your option) any later -;; version. -;; -;; This 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 General Public License -;; for more details. -;; -;; You should have received a copy of the GNU General Public License -;; along with GNU Emacs; see the file COPYING. If not, write to the -;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, -;; MA 02111-1307, USA. - -;;; Commentary: - -;; Coq is a proof assistant (http://coq.inria.fr/). This code run an -;; inferior Coq process and defines functions to send bits of code -;; from other buffers to the inferior process. This is a -;; customisation of comint-mode (see comint.el). For a more complex -;; and full featured Coq interface under Emacs look at Proof General -;; (http://zermelo.dcs.ed.ac.uk/~proofgen/). -;; -;; Written by Marco Maggesi <maggesi@math.unifi.it> with code heavly -;; borrowed from emacs cmuscheme.el -;; -;; Please send me bug reports, bug fixes, and extensions, so that I can -;; merge them into the master source. - -;;; Installation: - -;; You need to have gallina.el already installed (it comes with the -;; standard Coq distribution) in order to use this code. Put this -;; file somewhere in you load-path and add the following lines in your -;; "~/.emacs": -;; -;; (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) -;; (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) -;; (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t) -;; (autoload 'run-coq-other-window "inferior-coq" -;; "Run an inferior Coq process in a new window." t) -;; (autoload 'run-coq-other-frame "inferior-coq" -;; "Run an inferior Coq process in a new frame." t) - -;;; Usage: - -;; Call `M-x "run-coq'. -;; -;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'): -;; C-return ('M-x coq-send-line) send the current line. -;; C-c C-r (`M-x coq-send-region') send the current region. -;; C-c C-a (`M-x coq-send-abort') send the command "Abort". -;; C-c C-t (`M-x coq-send-restart') send the command "Restart". -;; C-c C-s (`M-x coq-send-show') send the command "Show". -;; C-c C-u (`M-x coq-send-undo') send the command "Undo". -;; C-c C-v (`M-x coq-check-region') run command "Check" on region. -;; C-c . (`M-x coq-come-here') Restart and send until current point. - -;;; Change Log: - -;; From -0.0 to 1.0 brought into existence. - - -(require 'gallina) -(require 'comint) - -(setq coq-program-name "coqtop") - -(defgroup inferior-coq nil - "Run a coq process in a buffer." - :group 'coq) - -(defcustom inferior-coq-mode-hook nil - "*Hook for customising inferior-coq mode." - :type 'hook - :group 'coq) - -(defvar inferior-coq-mode-map - (let ((m (make-sparse-keymap))) - (define-key m "\C-c\C-r" 'coq-send-region) - (define-key m "\C-c\C-a" 'coq-send-abort) - (define-key m "\C-c\C-t" 'coq-send-restart) - (define-key m "\C-c\C-s" 'coq-send-show) - (define-key m "\C-c\C-u" 'coq-send-undo) - (define-key m "\C-c\C-v" 'coq-check-region) - m)) - -;; Install the process communication commands in the coq-mode keymap. -(define-key coq-mode-map [(control return)] 'coq-send-line) -(define-key coq-mode-map "\C-c\C-r" 'coq-send-region) -(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort) -(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart) -(define-key coq-mode-map "\C-c\C-s" 'coq-send-show) -(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo) -(define-key coq-mode-map "\C-c\C-v" 'coq-check-region) -(define-key coq-mode-map "\C-c." 'coq-come-here) - -(defvar coq-buffer) - -(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq" - "\ -Major mode for interacting with an inferior Coq process. - -The following commands are available: -\\{inferior-coq-mode-map} - -A Coq process can be fired up with M-x run-coq. - -Customisation: Entry to this mode runs the hooks on comint-mode-hook -and inferior-coq-mode-hook (in that order). - -You can send text to the inferior Coq process from other buffers -containing Coq source. - -Functions and key bindings (Learn more keys with `C-c C-h'): - C-return ('M-x coq-send-line) send the current line. - C-c C-r (`M-x coq-send-region') send the current region. - C-c C-a (`M-x coq-send-abort') send the command \"Abort\". - C-c C-t (`M-x coq-send-restart') send the command \"Restart\". - C-c C-s (`M-x coq-send-show') send the command \"Show\". - C-c C-u (`M-x coq-send-undo') send the command \"Undo\". - C-c C-v (`M-x coq-check-region') run command \"Check\" on region. - C-c . (`M-x coq-come-here') Restart and send until current point. -" - ;; Customise in inferior-coq-mode-hook - (setq comint-prompt-regexp "^[^<]* < *") - (coq-mode-variables) - (setq mode-line-process '(":%s")) - (setq comint-input-filter (function coq-input-filter)) - (setq comint-get-old-input (function coq-get-old-input))) - -(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'" - "*Input matching this regexp are not saved on the history list. -Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters." - :type 'regexp - :group 'inferior-coq) - -(defun coq-input-filter (str) - "Don't save anything matching `inferior-coq-filter-regexp'." - (not (string-match inferior-coq-filter-regexp str))) - -(defun coq-get-old-input () - "Snarf the sexp ending at point." - (save-excursion - (let ((end (point))) - (backward-sexp) - (buffer-substring (point) end)))) - -(defun coq-args-to-list (string) - (let ((where (string-match "[ \t]" string))) - (cond ((null where) (list string)) - ((not (= where 0)) - (cons (substring string 0 where) - (coq-args-to-list (substring string (+ 1 where) - (length string))))) - (t (let ((pos (string-match "[^ \t]" string))) - (if (null pos) - nil - (coq-args-to-list (substring string pos - (length string))))))))) - -;;;###autoload -(defun run-coq (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (switch-to-buffer "*coq*")) -;;;###autoload (add-hook 'same-window-buffer-names "*coq*") - -;;;###autoload -(defun run-coq-other-window (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (pop-to-buffer "*coq*")) -;;;###autoload (add-hook 'same-window-buffer-names "*coq*") - -(defun run-coq-other-frame (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (switch-to-buffer-other-frame "*coq*")) - -(defun switch-to-coq (eob-p) - "Switch to the coq process buffer. -With argument, position cursor at end of buffer." - (interactive "P") - (if (get-buffer coq-buffer) - (pop-to-buffer coq-buffer) - (error "No current process buffer. See variable `coq-buffer'")) - (cond (eob-p - (push-mark) - (goto-char (point-max))))) - -(defun coq-send-region (start end) - "Send the current region to the inferior Coq process." - (interactive "r") - (comint-send-region (coq-proc) start end) - (comint-send-string (coq-proc) "\n")) - -(defun coq-send-line () - "Send the current line to the Coq process." - (interactive) - (save-excursion - (end-of-line) - (let ((end (point))) - (beginning-of-line) - (coq-send-region (point) end))) - (next-line 1)) - -(defun coq-send-abort () - "Send the command \"Abort.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Abort.\n")) - -(defun coq-send-restart () - "Send the command \"Restart.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Restart.\n")) - -(defun coq-send-undo () - "Reset coq to the initial state and send the region between the - beginning of file and the point." - (interactive) - (comint-send-string (coq-proc) "Undo.\n")) - -(defun coq-check-region (start end) - "Run the commmand \"Check\" on the current region." - (interactive "r") - (comint-proc-query (coq-proc) - (concat "Check " - (buffer-substring start end) - ".\n"))) - -(defun coq-send-show () - "Send the command \"Show.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Show.\n")) - -(defun coq-come-here () - "Reset coq to the initial state and send the region between the - beginning of file and the point." - (interactive) - (comint-send-string (coq-proc) "Reset Initial.\n") - (coq-send-region 1 (point))) - -(defvar coq-buffer nil "*The current coq process buffer.") - -(defun coq-proc () - "Return the current coq process. See variable `coq-buffer'." - (let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode) - (current-buffer) - coq-buffer)))) - (or proc - (error "No current process. See variable `coq-buffer'")))) - -(defcustom inferior-coq-load-hook nil - "This hook is run when inferior-coq is loaded in. -This is a good place to put keybindings." - :type 'hook - :group 'inferior-coq) - -(run-hooks 'inferior-coq-load-hook) - -(provide 'inferior-coq) 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 125c1452d5..155296362f 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 } @@ -116,8 +111,18 @@ let error_cannot_parse s (i,j) = Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j; exit 1 +let same_path_opt s s' = + let nf s = (* ./foo/a.ml and foo/a.ml are the same file *) + if Filename.is_implicit s + then "." // s + else s + in + let s = match s with None -> "." | Some s -> nf s in + let s' = match s' with None -> "." | Some s' -> nf s' in + s = s' + let warning_ml_clash x s suff s' suff' = - if suff = suff' then + if suff = suff' && not (same_path_opt s s') then eprintf "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff (match s with None -> "." | Some d -> d) @@ -140,9 +145,9 @@ let mllibAccu = ref ([] : (string * dir) list) let mlpackAccu = ref ([] : (string * dir) list) let add_caml_known phys_dir f = - let basename,suff = get_extension f [".ml";".ml4";".mlpack"] in + let basename,suff = get_extension f [".ml";".ml4";".mlg";".mlpack"] in match suff with - | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () @@ -194,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 |