From 48219205d121ea3093287ac1b887fc81067fac6a Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 15 Jun 2017 10:13:37 +0200 Subject: coqdep: correct support of Local Declare ML Module --- tools/coqdep_lexer.mll | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index c68c34bbbd..9224cdafe8 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -74,7 +74,9 @@ let dot = '.' ( space+ | eof) rule coq_action = parse | "Require" space+ { require_modifiers None lexbuf } - | "Local"? "Declare" space+ "ML" space+ "Module" space+ + | "Local" space+ "Declare" space+ "ML" space+ "Module" space+ + { modules [] lexbuf } + | "Declare" space+ "ML" space+ "Module" space+ { modules [] lexbuf } | "Load" space+ { load_file lexbuf } -- cgit v1.2.3 From da62d0dd86fc140ff58d9366a7a85e9b21b104b9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 14 Jun 2017 14:14:41 -0400 Subject: Strip trailing whitespace --- tools/CoqMakefile.in | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 5e223a0b48..bf0669578d 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -5,7 +5,7 @@ ## // # ## ############################################################################### ## GNUMakefile for Coq @COQ_VERSION@ - + # For debugging purposes (must stay here, don't move below) INITIAL_VARS := $(.VARIABLES) # To implement recursion we save the name of the main Makefile @@ -80,7 +80,7 @@ CAMLOPTLINK ?= $(OCAMLFIND) opt -rectypes -thread CAMLDEP ?= $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack # DESTDIR is prepended to all installation paths -DESTDIR ?= +DESTDIR ?= # Debug builds, typically -g to OCaml, -debug to Coq. CAMLDEBUG ?= @@ -96,7 +96,7 @@ COQDEBUG ?= # # post-all:: # echo "All done!" -# +# # in @LOCAL_FILE@ # ############################################################################### @@ -106,7 +106,7 @@ COQDEBUG ?= # Flags ####################################################################### # -# We define a bunch of variables combining the parameters +# We define a bunch of variables combining the parameters SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) @@ -127,7 +127,7 @@ DYNLIB:=.cmxs endif COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) -COQCHKFLAGS?=-silent -o $(COQLIBS) +COQCHKFLAGS?=-silent -o $(COQLIBS) COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that @@ -155,7 +155,7 @@ COQLIBINSTALL = $(COQLIB)user-contrib COQDOCINSTALL = $(DOCDIR)user-contrib COQTOPINSTALL = $(COQLIB)toploop -# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not) +# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not) ifneq "$(DSTROOT)" "" DESTDIR := $(DSTROOT) endif @@ -248,7 +248,7 @@ ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) # Compilation targets ######################################################### -all: +all: $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all @@ -427,10 +427,10 @@ clean:: $(HIDE)rm -f $(CMOFILES) $(HIDE)rm -f $(CMIFILES) $(HIDE)rm -f $(CMAFILES) - $(HIDE)rm -f $(CMOFILES:.cmo=.cmx) + $(HIDE)rm -f $(CMOFILES:.cmo=.cmx) $(HIDE)rm -f $(CMXAFILES) - $(HIDE)rm -f $(CMXSFILES) - $(HIDE)rm -f $(CMOFILES:.cmo=.o) + $(HIDE)rm -f $(CMXSFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.o) $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) $(HIDE)rm -f $(ALLDFILES) $(HIDE)rm -f $(ALLNATIVEFILES) @@ -513,7 +513,7 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack $(SHOW)'CAMLOPT -pack -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ -# This rule is for _CoqProject with no .mllib nor .mlpack +# 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 $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< @@ -600,7 +600,7 @@ byte: opt: $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" -.PHONY: opt +.PHONY: opt # This is deprecated. To extend this makefile use # extension points and @LOCAL_FILE@ @@ -655,4 +655,3 @@ debug: .PHONY: debug .DEFAULT_GOAL := all - -- cgit v1.2.3 From 15d61838d7435b45559d648bcde1ccfb6e468bcd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 7 Jun 2017 15:54:37 -0400 Subject: Fix `make TIMED=1` garbage It should not emit ` (user: 0.00 mem: 2852 ko)` multiple times--- tools/CoqMakefile.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index bf0669578d..f3a645a21e 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -132,7 +132,7 @@ COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile -COQ_VERSION:=$(shell $(COQC) --print-version | cut -d ' ' -f 1) +COQ_VERSION:=$(shell $(COQC) --print-version 2>/dev/null | cut -d ' ' -f 1) COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -- cgit v1.2.3 From cff08a2ec4f4cf100ecd0e30a6c9202b9defa9a9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 14 Jun 2017 14:16:47 -0400 Subject: Move TIMER to right in front of COQC Save the COQC variable for the actual path to coqc, as per https://github.com/coq/coq/pull/742#pullrequestreview-44072778 --- tools/CoqMakefile.in | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f3a645a21e..7b01c1b663 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -65,8 +65,8 @@ TIMECMD?= STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" # Coq binaries -COQC ?= $(TIMER) "$(COQBIN)coqc" -COQCHK ?= $(TIMER) "$(COQBIN)coqchk" +COQC ?= "$(COQBIN)coqc" +COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" @@ -132,7 +132,7 @@ COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile -COQ_VERSION:=$(shell $(COQC) --print-version 2>/dev/null | cut -d ' ' -f 1) +COQ_VERSION:=$(shell $(COQC) --print-version | cut -d ' ' -f 1) COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") @@ -281,17 +281,17 @@ quick: $(VOFILES:.vo=.vio) .PHONY: quick vio2vo: - $(COQC) $(COQDEBUG) $(COQFLAGS) \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo checkproofs: - $(COQC) $(COQDEBUG) $(COQFLAGS) \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) .PHONY: checkproofs validate: $(VOFILES) - $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=)) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=)) .PHONY: validate only: $(TGTS) @@ -520,19 +520,19 @@ $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix $(VOFILES): %.vo: %.v $(SHOW)COQC $< - $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< # FIXME ?merge with .vo / .vio ? $(GLOBFILES): %.glob: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $< + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< $(VFILES:.v=.vio): %.vio: %.v $(SHOW)COQC -quick $< - $(HIDE)$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< + $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< $(BEAUTYFILES): %.v.beautified: %.v $(SHOW)'BEAUTIFY $<' - $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $< $(GFILES): %.g: %.v $(SHOW)'GALLINA $<' -- cgit v1.2.3 From d8874dd855d748aaaf504890487ab15ffd7a677d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 11:41:40 +0200 Subject: [ide] Add route_id parameter to query call. This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####. --- tools/fake_ide.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'tools') diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 932097607b..4dad16fd8c 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -247,16 +247,16 @@ let eval_print l coq = 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 (phrase,tip_id())) coq + 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 (phrase, to_id)) coq + eval_call (query (0,(phrase, to_id))) coq | [ Tok(_,"WAIT") ] -> let phrase = "Stm Wait." in - eval_call (query (phrase,tip_id())) coq + eval_call (query (0,(phrase,tip_id()))) coq | [ Tok(_,"JOIN") ] -> let phrase = "Stm JoinDocument." in - eval_call (query (phrase,tip_id())) coq + eval_call (query (0,(phrase,tip_id()))) 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" -- cgit v1.2.3