diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index df8c343..c6a7ed7 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -23,6 +23,8 @@ jobs: - 'coqorg/coq:8.16' - 'coqorg/coq:8.17' - 'coqorg/coq:8.18' + - 'coqorg/coq:8.19' + - 'coqorg/coq:8.20' fail-fast: false steps: - uses: actions/checkout@v3 diff --git a/.gitignore b/.gitignore index 7271c20..f067213 100644 --- a/.gitignore +++ b/.gitignore @@ -34,3 +34,4 @@ nra.cache Makefile.coq* *~ *.conf +_build/ diff --git a/Makefile b/Makefile deleted file mode 100644 index 1d04bfc..0000000 --- a/Makefile +++ /dev/null @@ -1,26 +0,0 @@ -COQMAKEFILE?=Makefile.coq - -all: $(COQMAKEFILE) - @+$(MAKE) -f $^ $@ - -clean: $(COQMAKEFILE) - @+$(MAKE) -f $^ cleanall - @rm -f $^ $^.conf */*~ - $(MAKE) -C test $@ - -$(COQMAKEFILE): _CoqProject - $(COQBIN)coq_makefile -f $^ -o $@ - -test: - @+$(MAKE) -C test - -force _CoqProject Makefile: ; - -%: $(COQMAKEFILE) force - @+$(MAKE) -f $< $@ - -.PHONY: all clean force test - -publish%: - opam publish --packages-directory=released/packages \ - --repo=coq/opam-coq-archive --tag=v$* -v $* liyishuai/coq-parsec diff --git a/README.md b/README.md index 51543a4..34359da 100644 --- a/README.md +++ b/README.md @@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener [![Docker CI][docker-action-shield]][docker-action-link] -[docker-action-shield]: https://github.com/liyishuai/coq-parsec/workflows/Docker%20CI/badge.svg?branch=master -[docker-action-link]: https://github.com/liyishuai/coq-parsec/actions?query=workflow:"Docker%20CI" +[docker-action-shield]: https://github.com/liyishuai/coq-parsec/actions/workflows/docker-action.yml/badge.svg?branch=master +[docker-action-link]: https://github.com/liyishuai/coq-parsec/actions/workflows/docker-action.yml @@ -17,16 +17,17 @@ Inspired by Haskell Parsec library. ## Meta - Author(s): - - Yishuai Li [ORCID logo](https://orcid.org/0000-0002-5728-5903) + - Yishuai Li [ORCID logo](https://orcid.org/0000-0002-5728-5903) - Azzam Althagafi - - Yao Li [ORCID logo](https://orcid.org/0000-0001-8720-883X) - - Li-yao Xia [ORCID logo](https://orcid.org/0000-0003-2673-4400) - - Benjamin C. Pierce [ORCID logo](https://orcid.org/0000-0001-7839-1636) + - Yao Li [ORCID logo](https://orcid.org/0000-0001-8720-883X) + - Li-yao Xia [ORCID logo](https://orcid.org/0000-0003-2673-4400) + - Benjamin C. Pierce [ORCID logo](https://orcid.org/0000-0001-7839-1636) - License: [BSD 3-Clause "New" or "Revised" License](LICENSE) - Compatible Coq versions: 8.14 or later - Additional dependencies: - [Cérès](https://github.com/Lysxia/coq-ceres) - [ExtLib](https://coq-community.org/coq-ext-lib/) + - [Dune](https://dune.build) 2.5 or later - Coq namespace: `Parsec` - Related publication(s): none @@ -45,8 +46,8 @@ To instead build and install manually, do: ``` shell git clone https://github.com/liyishuai/coq-parsec.git cd coq-parsec -make # or make -j -make install +dune build +dune install ``` diff --git a/_CoqProject b/_CoqProject deleted file mode 100644 index 883b311..0000000 --- a/_CoqProject +++ /dev/null @@ -1,7 +0,0 @@ --R theories Parsec --arg -w -arg -local-declaration --native-compiler no - -theories/Parser.v -theories/Number.v -theories/Core.v diff --git a/coq-parsec.opam b/coq-parsec.opam index ca17cfa..ce94d2c 100644 --- a/coq-parsec.opam +++ b/coq-parsec.opam @@ -14,10 +14,9 @@ synopsis: "Monadic parser combinator library in Coq" description: """ Inspired by Haskell Parsec library.""" -build: [make "-j%{jobs}%"] -run-test: [make "-j%{jobs}%" "test"] -install: [make "install"] +build: ["dune" "build" "-p" name "-j" jobs] depends: [ + "dune" {>= "3.6"} "coq" { >= "8.14~" } "coq-ceres" { >= "0.4.0" } "coq-ext-lib" { >= "0.11.3" } diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..2c7cad6 --- /dev/null +++ b/dune-project @@ -0,0 +1,3 @@ +(lang dune 3.6) +(using coq 0.6) +(name coq-parsec) diff --git a/meta.yml b/meta.yml index c7f3f05..35bf0af 100644 --- a/meta.yml +++ b/meta.yml @@ -34,7 +34,7 @@ dependencies: opam: name: coq-ext-lib version: '{ >= "0.11.3" }' -test_target: test +dune: true categories: - name: Computer Science/Data Types and Data Structures keywords: @@ -51,3 +51,5 @@ tested_coq_opam_versions: - version: '8.16' - version: '8.17' - version: '8.18' + - version: '8.19' + - version: '8.20' diff --git a/test/Makefile b/test/Makefile deleted file mode 100644 index cfe38b1..0000000 --- a/test/Makefile +++ /dev/null @@ -1,999 +0,0 @@ -########################################################################## -## # The Coq Proof Assistant / The Coq Development Team ## -## v # Copyright INRIA, CNRS and contributors ## -## /dev/null 2>/dev/null; echo $$?)) -STDTIME?=command time -f $(TIMEFMT) -else -ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=gtime -f $(TIMEFMT) -else -STDTIME?=command time -endif -endif -else -STDTIME?=command time -f $(TIMEFMT) -endif - -COQBIN?= -ifneq (,$(COQBIN)) -# add an ending / -COQBIN:=$(COQBIN)/ -endif - -# Coq binaries -COQC ?= "$(COQBIN)coqc" -COQTOP ?= "$(COQBIN)coqtop" -COQCHK ?= "$(COQBIN)coqchk" -COQNATIVE ?= "$(COQBIN)coqnative" -COQDEP ?= "$(COQBIN)coqdep" -COQDOC ?= "$(COQBIN)coqdoc" -COQPP ?= "$(COQBIN)coqpp" -COQMKFILE ?= "$(COQBIN)coq_makefile" -OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" - -# Timing scripts -COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py" -COQMAKE_BOTH_TIME_FILES ?= "$(COQCORELIB)/tools/make-both-time-files.py" -COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing-files.py" -BEFORE ?= -AFTER ?= - -# OCaml binaries -CAMLC ?= "$(OCAMLFIND)" ocamlc -c -CAMLOPTC ?= "$(OCAMLFIND)" opt -c -CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkall -CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkall -CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack - -# DESTDIR is prepended to all installation paths -DESTDIR ?= - -# Debug builds, typically -g to OCaml, -debug to Coq. -CAMLDEBUG ?= -COQDEBUG ?= - -# Extra packages to be linked in (as in findlib -package) -CAMLPKGS ?= -FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS) - -# Option for making timing files -TIMING?= -# Option for changing sorting of timing output file -TIMING_SORT_BY ?= auto -# Option for changing the fuzz parameter on the output file -TIMING_FUZZ ?= 0 -# Option for changing whether to use real or user time for timing tables -TIMING_REAL?= -# Option for including the memory column(s) -TIMING_INCLUDE_MEM?= -# Option for sorting by the memory column -TIMING_SORT_BY_MEM?= -# Output file names for timed builds -TIME_OF_BUILD_FILE ?= time-of-build.log -TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log -TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log -TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log -TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log -TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line - -TGTS ?= - -# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) -ifdef DSTROOT -DESTDIR := $(DSTROOT) -endif - -# Substitution of the path by appending $(DESTDIR) if needed. -# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. -windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) -destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) - -# Installation paths of libraries and documentation. -COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) -COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/coq/user-contrib) -COQPLUGININSTALL ?= $(call destination_path,$(COQCORELIB)/..) -COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? - -# findlib files installation -FINDLIBPREINST= mkdir -p "$(COQPLUGININSTALL)/" -FINDLIBDESTDIR= -destdir "$(COQPLUGININSTALL)/" - -# we need to move out of sight $(METAFILE) otherwise findlib thinks the -# package is already installed -findlib_install = \ - $(HIDE)if [ "$(METAFILE)" ]; then \ - $(FINDLIBPREINST) && \ - mv "$(METAFILE)" "$(METAFILE).skip" ; \ - "$(OCAMLFIND)" install $(2) $(FINDLIBDESTDIR) $(FINDLIBPACKAGE) $(1); \ - rc=$$?; \ - mv "$(METAFILE).skip" "$(METAFILE)"; \ - exit $$rc; \ - fi -findlib_remove = \ - $(HIDE)if [ ! -z "$(METAFILE)" ]; then\ - "$(OCAMLFIND)" remove $(FINDLIBDESTDIR) $(FINDLIBPACKAGE); \ - fi - - -########## End of parameters ################################################## -# What follows may be relevant to you only if you need to -# extend this Makefile. If so, look for 'Extension point' here and -# put in Makefile.local double colon rules accordingly. -# E.g. to perform some work after the all target completes you can write -# -# post-all:: -# echo "All done!" -# -# in Makefile.local -# -############################################################################### - - - - -# Flags ####################################################################### -# -# We define a bunch of variables combining the parameters. -# To add additional flags to coq, coqchk or coqdoc, set the -# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add. -# To overwrite the default choice and set your own flags entirely, set the -# {COQ,COQCHK,COQDOC}FLAGS variable. - -SHOW := $(if $(VERBOSE),@true "",@echo "") -HIDE := $(if $(VERBOSE),,@) - -TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) - -OPT?= - -# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d -ifeq '$(OPT)' '-byte' -USEBYTE:=true -DYNOBJ:=.cma -DYNLIB:=.cma -else -USEBYTE:= -DYNOBJ:=.cmxs -DYNLIB:=.cmxs -endif - -# these variables are meant to be overridden if you want to add *extra* flags -COQEXTRAFLAGS?= -COQCHKEXTRAFLAGS?= -COQDOCEXTRAFLAGS?= - -# Find the last argument of the form "-native-compiler FLAG" -COQUSERNATIVEFLAG:=$(strip \ -$(subst -native-compiler-,,\ -$(lastword \ -$(filter -native-compiler-%,\ -$(subst -native-compiler ,-native-compiler-,\ -$(strip $(COQEXTRAFLAGS))))))) - -COQFILTEREDEXTRAFLAGS:=$(strip \ -$(filter-out -native-compiler-%,\ -$(subst -native-compiler ,-native-compiler-,\ -$(strip $(COQEXTRAFLAGS))))) - -COQACTUALNATIVEFLAG:=$(lastword $(COQMF_COQ_NATIVE_COMPILER_DEFAULT) $(COQMF_COQPROJECTNATIVEFLAG) $(COQUSERNATIVEFLAG)) - -ifeq '$(COQACTUALNATIVEFLAG)' 'yes' - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" - COQDONATIVE="yes" -else -ifeq '$(COQACTUALNATIVEFLAG)' 'ondemand' - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" - COQDONATIVE="no" -else - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "no" - COQDONATIVE="no" -endif -endif - -# these flags do NOT contain the libraries, to make them easier to overwrite -COQFLAGS?=-q $(OTHERFLAGS) $(COQFILTEREDEXTRAFLAGS) $(COQNATIVEFLAG) -COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) -COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) - -COQDOCLIBS?=$(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) -COQMAKEFILE_VERSION:=8.19.2 - -# COQ_SRC_SUBDIRS is for user-overriding, usually to add -# `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for -# Coq's own core libraries, which should be replaced by ocamlfind -# options at some point. -COQ_SRC_SUBDIRS?= -COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") - -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -# ocamldoc fails with unknown argument otherwise -CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) -CAMLFLAGS+=$(OCAMLWARN) - -ifneq (,$(TIMING)) - ifeq (after,$(TIMING)) - TIMING_EXT=after-timing - else - ifeq (before,$(TIMING)) - TIMING_EXT=before-timing - else - TIMING_EXT=timing - endif - endif - TIMING_ARG=-time-file $<.$(TIMING_EXT) -else - TIMING_ARG= -endif - -ifneq (,$(PROFILING)) - PROFILE_ARG=-profile $<.prof.json - PROFILE_ZIP=gzip $<.prof.json -else - PROFILE_ARG= - PROFILE_ZIP=true -endif - -# Files ####################################################################### -# -# We here define a bunch of variables about the files being part of the -# Coq project in order to ease the writing of build target and build rules - -VDFILE := .Makefile.d - -ALLSRCFILES := \ - $(MLGFILES) \ - $(MLFILES) \ - $(MLPACKFILES) \ - $(MLLIBFILES) \ - $(MLIFILES) - -# helpers -vo_to_obj = $(addsuffix .o,\ - $(filter-out Warning: Error:,\ - $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) -strip_dotslash = $(patsubst ./%,%,$(1)) - -# without this we get undefined variables in the expansion for the -# targets of the [deprecated,use-mllib-or-mlpack] rule -with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) - -VO = vo -VOS = vos - -VOFILES = $(VFILES:.v=.$(VO)) -GLOBFILES = $(VFILES:.v=.glob) -HTMLFILES = $(VFILES:.v=.html) -GHTMLFILES = $(VFILES:.v=.g.html) -BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) -TEXFILES = $(VFILES:.v=.tex) -GTEXFILES = $(VFILES:.v=.g.tex) -CMOFILES = \ - $(MLGFILES:.mlg=.cmo) \ - $(MLFILES:.ml=.cmo) \ - $(MLPACKFILES:.mlpack=.cmo) -CMXFILES = $(CMOFILES:.cmo=.cmx) -OFILES = $(CMXFILES:.cmx=.o) -CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) -CMXAFILES = $(CMAFILES:.cma=.cmxa) -CMIFILES = \ - $(CMOFILES:.cmo=.cmi) \ - $(MLIFILES:.mli=.cmi) -# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just -# a .mlg file -CMXSFILES = \ - $(MLPACKFILES:.mlpack=.cmxs) \ - $(CMXAFILES:.cmxa=.cmxs) \ - $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) - -# files that are packed into a plugin (no extension) -PACKEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) -# files that are archived into a .cma (mllib) -LIBEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) -CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) -CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) -OBJFILES = $(call vo_to_obj,$(VOFILES)) -ALLNATIVEFILES = \ - $(OBJFILES:.o=.cmi) \ - $(OBJFILES:.o=.cmx) \ - $(OBJFILES:.o=.cmxs) -FINDLIBPACKAGE=$(patsubst .%,%,$(suffix $(METAFILE))) - -# trick: wildcard filters out non-existing files, so that `install` doesn't show -# warnings and `clean` doesn't pass to rm a list of files that is too long for -# the shell. -NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) -FILESTOINSTALL = \ - $(VOFILES) \ - $(VFILES) \ - $(GLOBFILES) \ - $(NATIVEFILES) \ - $(CMXSFILES) # to be removed when we remove legacy loading -FINDLIBFILESTOINSTALL = \ - $(CMIFILESTOINSTALL) -ifeq '$(HASNATDYNLINK)' 'true' -DO_NATDYNLINK = yes -FINDLIBFILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) -else -DO_NATDYNLINK = -endif - -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) - -# Compilation targets ######################################################### - -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 -.PHONY: all - -all.timing.diff: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all -.PHONY: all.timing.diff - -ifeq (0,$(TIMING_REAL)) -TIMING_REAL_ARG := -TIMING_USER_ARG := --user -else -ifeq (1,$(TIMING_REAL)) -TIMING_REAL_ARG := --real -TIMING_USER_ARG := -else -TIMING_REAL_ARG := -TIMING_USER_ARG := -endif -endif - -ifeq (0,$(TIMING_INCLUDE_MEM)) -TIMING_INCLUDE_MEM_ARG := --no-include-mem -else -TIMING_INCLUDE_MEM_ARG := -endif - -ifeq (1,$(TIMING_SORT_BY_MEM)) -TIMING_SORT_BY_MEM_ARG := --sort-by-mem -else -TIMING_SORT_BY_MEM_ARG := -endif - -make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) -make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) -make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: - $(HIDE)rm -f pretty-timed-success.ok - $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) - $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed -print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(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) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(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 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 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) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -endif -endif -pretty-timed: - $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed -.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff - -# Extension points for actions to be performed before/after the all target -pre-all:: - @# Extension point - $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ - echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ - echo "W: while the current Coq version is $(COQ_VERSION)";\ - fi -.PHONY: pre-all - -post-all:: - @# Extension point -.PHONY: post-all - -real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) -.PHONY: real-all - -real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONY: real-all.timing.diff - -bytefiles: $(CMOFILES) $(CMAFILES) -.PHONY: bytefiles - -optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) -.PHONY: optfiles - -# FIXME, see Ralf's bugreport -# quick is deprecated, now renamed vio -vio: $(VOFILES:.vo=.vio) -.PHONY: vio -quick: vio - $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") -.PHONY: quick - -vio2vo: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -.PHONY: vio2vo - -# quick2vo is undocumented -quick2vo: - $(HIDE)make -j $(J) vio - $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ - viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ - if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ - done); \ - echo "VIO2VO: $$VIOFILES"; \ - if [ -n "$$VIOFILES" ]; then \ - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ - fi -.PHONY: quick2vo - -checkproofs: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -.PHONY: checkproofs - -vos: $(VOFILES:%.vo=%.vos) -.PHONY: vos - -vok: $(VOFILES:%.vo=%.vok) -.PHONY: vok - -validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ -.PHONY: validate - -only: $(TGTS) -.PHONY: only - -# Documentation targets ####################################################### - -html: $(GLOBFILES) $(VFILES) - $(SHOW)'COQDOC -d html $(GAL)' - $(HIDE)mkdir -p html - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) - -mlihtml: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -d $@' - $(HIDE)mkdir $@ || rm -rf $@/* - $(HIDE)$(CAMLDOC) -html \ - -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) - -all-mli.tex: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -latex $@' - $(HIDE)$(CAMLDOC) -latex \ - -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) - -all.ps: $(VFILES) - $(SHOW)'COQDOC -ps $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort $(VFILES)` - -all.pdf: $(VFILES) - $(SHOW)'COQDOC -pdf $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort $(VFILES)` - -# FIXME: not quite right, since the output name is different -gallinahtml: GAL=-g -gallinahtml: html - -all-gal.ps: GAL=-g -all-gal.ps: all.ps - -all-gal.pdf: GAL=-g -all-gal.pdf: all.pdf - -# ? -beautify: $(BEAUTYFILES) - for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done - @echo 'Do not do "make clean" until you are sure that everything went well!' - @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' -.PHONY: beautify - -# Installation targets ######################################################## -# -# There rules can be extended in Makefile.local -# Extensions can't assume when they run. - -# We use $(file) to avoid generating a very long command string to pass to the shell -# (cf https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Strange.20command.20length.20limit.20on.20Linux) -# However Apple ships old make which doesn't have $(file) so we need a fallback -$(file >.hasfile,1) -HASFILE:=$(shell if [ -e .hasfile ]; then echo 1; rm .hasfile; fi) - -MKFILESTOINSTALL= $(if $(HASFILE),$(file >.filestoinstall,$(FILESTOINSTALL)),\ - $(shell rm -f .filestoinstall) \ - $(foreach x,$(FILESTOINSTALL),$(shell printf '%s\n' "$x" >> .filestoinstall))) - -# findlib needs the package to not be installed, so we remove it before -# installing it (see the call to findlib_remove) -install: META - @$(MKFILESTOINSTALL) - $(HIDE)code=0; for f in $$(cat .filestoinstall); do\ - if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ - done; exit $$code - $(HIDE)for f in $$(cat .filestoinstall); do\ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ "$$?" != "0" -o -z "$$df" ]; then\ - echo SKIP "$$f" since it has no logical path;\ - else\ - install -d "$(COQLIBINSTALL)/$$df" &&\ - install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ - echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ - fi;\ - done - $(call findlib_remove) - $(call findlib_install, META $(FINDLIBFILESTOINSTALL)) - $(HIDE)$(MAKE) install-extra -f "$(SELF)" - @rm -f .filestoinstall -install-extra:: - @# Extension point -.PHONY: install install-extra - -META: $(METAFILE) - $(HIDE)if [ "$(METAFILE)" ]; then \ - cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \ - fi - -install-byte: - $(call findlib_install, $(CMAFILES) $(CMOFILESTOINSTALL), -add) - -install-doc:: html mlihtml - @# Extension point - $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(HIDE)for i in html/*; do \ - dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ - install -m 0644 "$$i" "$$dest";\ - echo INSTALL "$$i" "$$dest";\ - done - $(HIDE)install -d \ - "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE)for i in mlihtml/*; do \ - dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ - install -m 0644 "$$i" "$$dest";\ - echo INSTALL "$$i" "$$dest";\ - done -.PHONY: install-doc - -uninstall:: - @# Extension point - @$(MKFILESTOINSTALL) - $(call findlib_remove) - $(HIDE)for f in $$(cat .filestoinstall); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ - rm -f "$$instf" &&\ - echo RM "$$instf" ;\ - done - $(HIDE)for f in $$(cat .filestoinstall); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\ - (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ - done - @rm -f .filestoinstall - -.PHONY: uninstall - -uninstall-doc:: - @# Extension point - $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' - $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' - $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true -.PHONY: uninstall-doc - -# Cleaning #################################################################### -# -# There rules can be extended in Makefile.local -# Extensions can't assume when they run. - -clean:: - @# Extension point - $(SHOW)'CLEAN' - $(HIDE)rm -f $(CMOFILES) - $(HIDE)rm -f $(CMIFILES) - $(HIDE)rm -f $(CMAFILES) - $(HIDE)rm -f $(CMXFILES) - $(HIDE)rm -f $(CMXAFILES) - $(HIDE)rm -f $(CMXSFILES) - $(HIDE)rm -f $(OFILES) - $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) - $(HIDE)rm -f $(MLGFILES:.mlg=.ml) - $(HIDE)rm -f $(CMXFILES:.cmx=.cmt) - $(HIDE)rm -f $(MLIFILES:.mli=.cmti) - $(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 $(VOFILES:.vo=.vos) - $(HIDE)rm -f $(VOFILES:.vo=.vok) - $(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) - $(HIDE)rm -f $(VFILES:.v=.tex) - $(HIDE)rm -f $(VFILES:.v=.g.tex) - $(HIDE)rm -f pretty-timed-success.ok - $(HIDE)rm -f META - $(HIDE)rm -rf html mlihtml -.PHONY: clean - -cleanall:: clean - @# Extension point - $(SHOW)'CLEAN *.aux *.timing' - $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) - $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) - $(HIDE)rm -f $(VOFILES:.vo=.v.timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) - $(HIDE)rm -f .lia.cache .nia.cache -.PHONY: cleanall - -archclean:: - @# Extension point - $(SHOW)'CLEAN *.cmx *.o' - $(HIDE)rm -f $(NATIVEFILES) - $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) -.PHONY: archclean - - -# Compilation rules ########################################################### - -$(MLIFILES:.mli=.cmi): %.cmi: %.mli - $(SHOW)'CAMLC -c $<' - $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< - -$(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)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< - -# Same hack -$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml - $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $(FOR_PACK) $< - - -$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - -$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - - -$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx | %.mlpack - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< - -$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack - $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack - $(SHOW)'CAMLOPT -pack -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -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) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx - $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -# can't make -# https://www.gnu.org/software/make/manual/make.html#Static-Pattern -# work with multiple target rules -# so use eval in a loop instead -# with grouped targets https://www.gnu.org/software/make/manual/make.html#Multiple-Targets -# if available (GNU Make >= 4.3) -ifneq (,$(filter grouped-target,$(.FEATURES))) -define globvorule= - -# take care to $$ variables using $< etc - $(1).vo $(1).glob &: $(1).v | $$(VDFILE) - $$(SHOW)COQC $(1).v - $$(HIDE)$$(TIMER) $$(COQC) $$(COQDEBUG) $$(TIMING_ARG) $$(PROFILE_ARG) $$(COQFLAGS) $$(COQLIBS) $(1).v - $$(HIDE)$$(PROFILE_ZIP) -ifeq ($(COQDONATIVE), "yes") - $$(SHOW)COQNATIVE $(1).vo - $$(HIDE)$$(call TIMER,$(1).vo.native) $$(COQNATIVE) $$(COQLIBS) $(1).vo -endif - -endef -else - -$(VOFILES): %.vo: %.v | $(VDFILE) - $(SHOW)COQC $< - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $< - $(HIDE)$(PROFILE_ZIP) -ifeq ($(COQDONATIVE), "yes") - $(SHOW)COQNATIVE $@ - $(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@ -endif - -# this is broken :( todo fix if we ever find a solution that doesn't need grouped targets -$(GLOBFILES): %.glob: %.v - $(SHOW)'COQC $< (for .glob)' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -endif - -$(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile)))) - -$(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -vio $< - $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(VFILES:.v=.vos): %.vos: %.v - $(SHOW)COQC -vos $< - $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(VFILES:.v=.vok): %.vok: %.v - $(SHOW)COQC -vok $< - $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing - $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" - -$(BEAUTYFILES): %.v.beautified: %.v - $(SHOW)'BEAUTIFY $<' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< - -$(TEXFILES): %.tex: %.v - $(SHOW)'COQDOC -latex $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ - -$(GTEXFILES): %.g.tex: %.v - $(SHOW)'COQDOC -latex -g $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ - -$(HTMLFILES): %.html: %.v %.glob - $(SHOW)'COQDOC -html $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ - -$(GHTMLFILES): %.g.html: %.v %.glob - $(SHOW)'COQDOC -html -g $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ - -# Dependency files ############################################################ - -ifndef MAKECMDGOALS - -include $(ALLDFILES) -else - ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) - -include $(ALLDFILES) - endif -endif - -.SECONDARY: $(ALLDFILES) - -redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) - -GENMLFILES:=$(MLGFILES:.mlg=.ml) -$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) - -$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(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) - -$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) - -# If this makefile is created using a _CoqProject we have coqdep get -# options from it. This avoids argument length limits for pathological -# projects. Note that extra options might be on the command line. -VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) - -$(VDFILE): _CoqProject $(VFILES) - $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) - -# Misc ######################################################################## - -byte: - $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" -.PHONY: byte - -opt: - $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" -.PHONY: opt - -# This is deprecated. To extend this makefile use -# extension points and Makefile.local -printenv:: - $(warning printenv is deprecated) - $(warning write extensions in Makefile.local or include Makefile.conf) - @echo 'COQLIB = $(COQLIB)' - @echo 'COQCORELIB = $(COQCORELIB)' - @echo 'DOCDIR = $(DOCDIR)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' - @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' - @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' - @echo 'COQCORE_SRC_SUBDIRS = $(COQCORE_SRC_SUBDIRS)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'PP = $(PP)' - @echo 'COQFLAGS = $(COQFLAGS)' - @echo 'COQLIB = $(COQLIBS)' - @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' - @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' -.PHONY: printenv - -# Generate a .merlin file. If you need to append directives to this -# file you can extend the merlin-hook target in Makefile.local -.merlin: - $(SHOW)'FILL .merlin' - $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin - $(HIDE)echo 'B $(COQCORELIB)' >> .merlin - $(HIDE)echo 'S $(COQCORELIB)' >> .merlin - $(HIDE)$(foreach d,$(COQCORE_SRC_SUBDIRS), \ - echo 'B $(COQCORELIB)$(d)' >> .merlin;) - $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo 'S $(COQLIB)$(d)' >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) - $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" -.PHONY: merlin - -merlin-hook:: - @# Extension point -.PHONY: merlin-hook - -# prints all variables -debug: - $(foreach v,\ - $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ - $(.VARIABLES))),\ - $(info $(v) = $($(v)))) -.PHONY: debug - -.DEFAULT_GOAL := all - -# Users can create Makefile.local-late to hook into double-colon rules -# or add other needed Makefile code, using defined -# variables if necessary. --include Makefile.local-late - -# Local Variables: -# mode: makefile-gmake -# End: diff --git a/test/_CoqProject b/test/_CoqProject deleted file mode 100644 index f58af55..0000000 --- a/test/_CoqProject +++ /dev/null @@ -1,5 +0,0 @@ --Q ../theories Parsec - -Number.v -Token.v -Chunk.v diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..08db430 --- /dev/null +++ b/test/dune @@ -0,0 +1,20 @@ +(alias + (name runtest) + (deps + (package coq-parsec) + (alias_rec all))) + +(rule + (alias runtest) + (action + (run coqc %{dep:Chunk.v}))) + +(rule + (alias runtest) + (action + (run coqc %{dep:Number.v}))) + +(rule + (alias runtest) + (action + (run coqc %{dep:Token.v}))) diff --git a/theories/dune b/theories/dune new file mode 100644 index 0000000..8533ec0 --- /dev/null +++ b/theories/dune @@ -0,0 +1,7 @@ +; This file was generated from `meta.yml`, please do not edit manually. +; Follow the instructions on https://github.com/coq-community/templates to regenerate. + +(coq.theory + (name Parsec) + (package coq-parsec) + (synopsis "Monadic parser combinator library in Coq"))