diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2019-03-05 17:18:15 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2019-03-05 17:18:15 +0100 |
commit | 33010bfa6345549d8b9b0c06f44150b60d0c86e5 (patch) | |
tree | 343dcf7c5dd696bd69610e7b0b464dcd70c4ca60 | |
parent | b96d222d47da5c5d59b65dfa152e255b7a4f7b46 (diff) | |
download | smtcoq-33010bfa6345549d8b9b0c06f44150b60d0c86e5.tar.gz smtcoq-33010bfa6345549d8b9b0c06f44150b60d0c86e5.zip |
No hard-coded paths to executables (fixes #37)
-rwxr-xr-x | src/configure.sh | 6 | ||||
-rw-r--r-- | src/versions/standard/Make | 4 | ||||
-rw-r--r-- | src/versions/standard/Makefile | 782 | ||||
-rw-r--r-- | src/versions/standard/Makefile.conf | 103 |
4 files changed, 6 insertions, 889 deletions
diff --git a/src/configure.sh b/src/configure.sh index cc2a1ca..85571cd 100755 --- a/src/configure.sh +++ b/src/configure.sh @@ -2,7 +2,9 @@ pre=$(echo $0 | sed "s,\(\([^/]*/\)*\)[^/]*,\1,") +rm -f ${pre}Make rm -f ${pre}Makefile +rm -f ${pre}Makefile.conf rm -f ${pre}smtcoq_plugin.ml4 rm -f ${pre}versions/native/Structures.v rm -f ${pre}g_smtcoq.ml4 @@ -22,8 +24,6 @@ if [ $@ -a $@ = -native ]; then cp ${pre}versions/native/Structures_native.v ${pre}versions/native/Structures.v else cp ${pre}versions/standard/Make ${pre}Make - cp ${pre}versions/standard/Makefile ${pre}Makefile - cp ${pre}versions/standard/Makefile.conf ${pre}Makefile.conf cp ${pre}versions/standard/g_smtcoq_standard.ml4 ${pre}g_smtcoq.ml4 cp ${pre}versions/standard/smtcoq_plugin_standard.mlpack ${pre}smtcoq_plugin.mlpack cp ${pre}versions/standard/Int63/Int63_standard.v ${pre}versions/standard/Int63/Int63.v @@ -33,4 +33,6 @@ else cp ${pre}versions/standard/Int63/Int63Properties_standard.v ${pre}versions/standard/Int63/Int63Properties.v cp ${pre}versions/standard/Array/PArray_standard.v ${pre}versions/standard/Array/PArray.v cp ${pre}versions/standard/Structures_standard.v ${pre}versions/standard/Structures.v + coq_makefile -f Make -o Makefile + sed -i Makefile -e "s/ocamldep/ocamldep -native/" -e "s/ \$(HIDE)\$(MAKE) --no-print-directory -f \"\$(SELF)\" post-all//" fi diff --git a/src/versions/standard/Make b/src/versions/standard/Make index e47c530..543d6f0 100644 --- a/src/versions/standard/Make +++ b/src/versions/standard/Make @@ -1,6 +1,6 @@ ######################################################################## -## This file is intended to developers, please do not use it to ## -## generate a Makefile, rather use the provided Makefile. ## +## This file is intended to developers: please do not use it ## +## directly, rather use the "configure.sh" script. ## ######################################################################## diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile deleted file mode 100644 index 2337ad7..0000000 --- a/src/versions/standard/Makefile +++ /dev/null @@ -1,782 +0,0 @@ -############################################################################### -## v # The Coq Proof Assistant ## -## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## -## \VV/ # ## -## // # ## -############################################################################### -## GNUMakefile for Coq 8.7.2 - -# For debugging purposes (must stay here, don't move below) -INITIAL_VARS := $(.VARIABLES) -# To implement recursion we save the name of the main Makefile -SELF := $(lastword $(MAKEFILE_LIST)) -PARENT := $(firstword $(MAKEFILE_LIST)) - -# This file is generated by coq_makefile and contains many variable -# definitions, like the list of .v files or the path to Coq -include Makefile.conf - -# Put in place old names -VFILES := $(COQMF_VFILES) -MLIFILES := $(COQMF_MLIFILES) -MLFILES := $(COQMF_MLFILES) -ML4FILES := $(COQMF_ML4FILES) -MLPACKFILES := $(COQMF_MLPACKFILES) -MLLIBFILES := $(COQMF_MLLIBFILES) -INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT) -OTHERFLAGS := $(COQMF_OTHERFLAGS) -COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS) -OCAMLLIBS := $(COQMF_OCAMLLIBS) -SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS) -COQLIBS := $(COQMF_COQLIBS) -COQLIBS_NOML := $(COQMF_COQLIBS_NOML) -LOCAL := $(COQMF_LOCAL) -COQLIB := $(COQMF_COQLIB) -DOCDIR := $(COQMF_DOCDIR) -OCAMLFIND := $(COQMF_OCAMLFIND) -CAMLP4 := $(COQMF_CAMLP4) -CAMLP4O := $(COQMF_CAMLP4O) -CAMLP4BIN := $(COQMF_CAMLP4BIN) -CAMLP4LIB := $(COQMF_CAMLP4LIB) -CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS) -CAMLFLAGS := $(COQMF_CAMLFLAGS) -HASNATDYNLINK := $(COQMF_HASNATDYNLINK) - -Makefile.conf: Make - coq_makefile -f Make -o Makefile - -# This file can be created by the user to hook into double colon rules or -# add any other Makefile code he may need --include Makefile.local - -# Parameters ################################################################## -# -# Parameters are make variable assignments. -# They can be passed to (each call to) make on the command line. -# They can also be put in Makefile.local once an for all. -# For retro-compatibility reasons they can be put in the _CoqProject, but this -# practice is discouraged since _CoqProject better not contain make specific -# code (be nice to user interfaces). - -# Print shell commands (set to non empty) -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 -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) -else -ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=gtime -f $(TIMEFMT) -else -STDTIME?=time -endif -endif -else -STDTIME?=/usr/bin/env time -f $(TIMEFMT) -endif - -# Coq binaries -COQC ?= "$(COQBIN)coqc" -COQTOP ?= "$(COQBIN)coqtop" -COQCHK ?= "$(COQBIN)coqchk" -COQDEP ?= "$(COQBIN)coqdep" -GALLINA ?= "$(COQBIN)gallina" -COQDOC ?= "$(COQBIN)coqdoc" -COQMKTOP ?= "$(COQBIN)coqmktop" -COQMKFILE ?= "$(COQBIN)coq_makefile" - -# Timing scripts -COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" -COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" -COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" -BEFORE ?= -AFTER ?= - -# FIXME this should be generated by Coq (modules already linked by Coq) -CAMLDONTLINK=camlp5.gramlib,unix,str - -# OCaml binaries -CAMLC ?= "$(OCAMLFIND)" ocamlc -c -CAMLOPTC ?= "$(OCAMLFIND)" opt -c -CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK) -CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK) -CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -CAMLDEP ?= "$(OCAMLFIND)" ocamldep -native -slash -ml-synonym .ml4 -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 ?= - -# Option for making timing files -TIMING?= -# 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 - -########## 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 - -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 - -COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) -COQCHKFLAGS?=-silent -o $(COQLIBS) -COQDOCFLAGS?=-interpolate -utf8 -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.7.2 - -COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") - -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) - -# 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 -ifeq ($(CAMLP4),camlp5) -CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo -else -CAMLP4EXTEND= -endif - -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 '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' -endif - -ifneq (,$(TIMING)) -TIMING_ARG=-time -ifeq (after,$(TIMING)) -TIMING_EXT=after-timing -else -ifeq (before,$(TIMING)) -TIMING_EXT=before-timing -else -TIMING_EXT=timing -endif -endif -else -TIMING_ARG= -endif - -# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) -ifdef DSTROOT -DESTDIR := $(DSTROOT) -endif - -concat_path = $(if $(1),$(1)/$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)) - -COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib) -COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib) -COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) - -# 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 - -ALLSRCFILES := \ - $(VFILES) \ - $(ML4FILES) \ - $(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)) -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)) -TEXFILES = $(VFILES:.v=.tex) -GTEXFILES = $(VFILES:.v=.g.tex) -CMOFILES = \ - $(ML4FILES:.ml4=.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 .ml4 file -CMXSFILES = \ - $(MLPACKFILES:.mlpack=.cmxs) \ - $(CMXAFILES:.cmxa=.cmxs) \ - $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(ML4FILES:.ml4=.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)),$($(lib)))) -# files that are archived into a .cma (mllib) -LIBEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(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) -# 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) \ - $(CMIFILESTOINSTALL) -BYTEFILESTOINSTALL = \ - $(CMOFILESTOINSTALL) \ - $(CMAFILES) -ifeq '$(HASNATDYNLINK)' 'true' -DO_NATDYNLINK = yes -FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) -else -DO_NATDYNLINK = -endif - -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) - -# Compilation targets ######################################################### - -all: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-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="" -.PHONY: all.timing.diff - -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) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_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' - $(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' - $(HIDE)false -else -print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(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) -.PHONE: real-all.timing.diff - -bytefiles: $(CMOFILES) $(CMAFILES) -.PHONY: bytefiles - -optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) -.PHONY: optfiles - -# FIXME, see Ralph's bugreport -quick: $(VOFILES:.vo=.vio) -.PHONY: quick - -vio2vo: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ - -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -.PHONY: vio2vo - -checkproofs: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ - -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -.PHONY: checkproofs - -validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=)) -.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) - -all-mli.tex: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -latex $@' - $(HIDE)$(CAMLDOC) -latex \ - -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) - -gallina: $(GFILES) - -all.ps: $(VFILES) - $(SHOW)'COQDOC -ps $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` - -all.pdf: $(VFILES) - $(SHOW)'COQDOC -pdf $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(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. - -install: - $(HIDE)for f in $(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 - $(HIDE)$(MAKE) install-extra -f "$(SELF)" -install-extra:: - @# Extension point -.PHONY: install install-extra - -install-byte: - $(HIDE)for f in $(BYTEFILESTOINSTALL); 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 - -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 - $(HIDE)for f in $(FILESTOINSTALL); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ - rm -f "$$instf" &&\ - echo RM "$$instf" &&\ - (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ - done -.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 $(CMOFILES:.cmo=.cmx) - $(HIDE)rm -f $(CMXAFILES) - $(HIDE)rm -f $(CMXSFILES) - $(HIDE)rm -f $(CMOFILES:.cmo=.o) - $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) - $(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) - $(HIDE)rm -f $(VFILES:.v=.tex) - $(HIDE)rm -f $(VFILES:.v=.g.tex) - $(HIDE)rm -f pretty-timed-success.ok - $(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) -.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)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< - -$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 - $(SHOW)'CAMLC -pp -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $< - -$(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 - $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< - -$(MLFILES:.ml=.cmx): %.cmx: %.ml - $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< - - -$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ - -linkall -shared -o $@ $< - -$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ - -$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ - - -$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ - -shared -linkall -o $@ $< - -$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< - -$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack - $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ - -$(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 -$(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) $(CAMLPKGS) \ - -shared -o $@ $< - -ifneq (,$(TIMING)) -TIMING_EXTRA = > $<.$(TIMING_EXT) -else -TIMING_EXTRA = -endif - -$(VOFILES): %.vo: %.v - $(SHOW)COQC $< - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA) - -# FIXME ?merge with .vo / .vio ? -$(GLOBFILES): %.glob: %.v - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< - -$(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -quick $< - $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< - -$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing - $(SHOW)PYTHON TIMING-DIFF $< - $(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) -beautify $< - -$(GFILES): %.g: %.v - $(SHOW)'GALLINA $<' - $(HIDE)$(GALLINA) $< - -$(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 ############################################################ - -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) -else - ifeq ($(MAKECMDGOALS),) - -include $(ALLDFILES) - endif -endif - -.SECONDARY: $(ALLDFILES) - -redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) - -$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 - $(SHOW)'CAMLDEP -pp $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) - -$(addsuffix .d,$(VFILES)): %.v.d: %.v - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(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 'LOCAL = $(LOCAL)' - @echo 'COQLIB = $(COQLIB)' - @echo 'DOCDIR = $(DOCDIR)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'CAMLP4 = $(CAMLP4)' - @echo 'CAMLP4O = $(CAMLP4O)' - @echo 'CAMLP4BIN = $(CAMLP4BIN)' - @echo 'CAMLP4LIB = $(CAMLP4LIB)' - @echo 'CAMLP4OPTIONS = $(CAMLP4OPTIONS)' - @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' - @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' - @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'PP = $(PP)' - @echo 'COQFLAGS = $(COQFLAGS)' - @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 $(COQLIB)' >> .merlin - $(HIDE)echo 'S $(COQLIB)' >> .merlin - $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo 'B $(COQLIB)$(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 diff --git a/src/versions/standard/Makefile.conf b/src/versions/standard/Makefile.conf deleted file mode 100644 index 928db7d..0000000 --- a/src/versions/standard/Makefile.conf +++ /dev/null @@ -1,103 +0,0 @@ -# This configuration file was generated by running: -# coq_makefile -f Make -o Makefile - - -############################################################################### -# # -# Project files. # -# # -############################################################################### - -COQMF_VFILES = versions/standard/Int63/Int63.v versions/standard/Int63/Int63Native.v versions/standard/Int63/Int63Op.v versions/standard/Int63/Int63Axioms.v versions/standard/Int63/Int63Properties.v versions/standard/Array/PArray.v versions/standard/Structures.v bva/BVList.v bva/Bva_checker.v classes/SMT_classes.v classes/SMT_classes_instances.v array/FArray.v array/Array_checker.v cnf/Cnf.v euf/Euf.v lia/Lia.v spl/Assumptions.v spl/Syntactic.v spl/Arithmetic.v spl/Operators.v Conversion_tactics.v Misc.v SMTCoq.v ReflectFacts.v PropToBool.v BoolToProp.v Tactics.v SMT_terms.v State.v Trace.v -COQMF_MLIFILES = versions/standard/structures.mli trace/coqTerms.mli trace/smtBtype.mli trace/satAtom.mli trace/smtAtom.mli trace/smtCertif.mli trace/smtCnf.mli trace/smtCommands.mli trace/smtForm.mli trace/smtMisc.mli trace/smtTrace.mli smtlib2/smtlib2_parse.mli smtlib2/smtlib2_lex.mli smtlib2/smtlib2_ast.mli smtlib2/smtlib2_genConstr.mli smtlib2/smtlib2_util.mli smtlib2/sExpr.mli smtlib2/smtlib2_solver.mli smtlib2/sExprParser.mli verit/veritParser.mli verit/veritLexer.mli verit/verit.mli verit/veritSyntax.mli lfsc/shashcons.mli lfsc/hstring.mli lfsc/lfscParser.mli lfsc/ast.mli lfsc/translator_sig.mli lfsc/tosmtcoq.mli zchaff/cnfParser.mli zchaff/satParser.mli zchaff/zchaff.mli zchaff/zchaffParser.mli lia/lia.mli -COQMF_MLFILES = versions/standard/structures.ml trace/coqTerms.ml trace/smtBtype.ml trace/satAtom.ml trace/smtAtom.ml trace/smtCertif.ml trace/smtCnf.ml trace/smtCommands.ml trace/smtForm.ml trace/smtMisc.ml trace/smtTrace.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/smtlib2_ast.ml smtlib2/smtlib2_genConstr.ml smtlib2/smtlib2_util.ml smtlib2/sExpr.ml smtlib2/smtlib2_solver.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml verit/veritParser.ml verit/veritLexer.ml verit/verit.ml verit/veritSyntax.ml lfsc/shashcons.ml lfsc/hstring.ml lfsc/lfscParser.ml lfsc/type.ml lfsc/ast.ml lfsc/builtin.ml lfsc/tosmtcoq.ml lfsc/converter.ml lfsc/lfsc.ml lfsc/lfscLexer.ml zchaff/cnfParser.ml zchaff/satParser.ml zchaff/zchaff.ml zchaff/zchaffParser.ml lia/lia.ml -COQMF_ML4FILES = g_smtcoq.ml4 -COQMF_MLPACKFILES = smtcoq_plugin.mlpack -COQMF_MLLIBFILES = - -############################################################################### -# # -# Path directives (-I, -R, -Q). # -# # -############################################################################### - -COQMF_OCAMLLIBS = -I . -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/standard -I versions/standard/Int63 -I versions/standard/Array -I '$(shell $(COQBIN)coqc -where)/plugins/micromega' -COQMF_SRC_SUBDIRS = . bva classes array cnf euf lfsc lia smtlib2 trace verit zchaff versions/standard versions/standard/Int63 versions/standard/Array '$(shell $(COQBIN)coqc -where)/plugins/micromega' -COQMF_COQLIBS = -I . -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/standard -I versions/standard/Int63 -I versions/standard/Array -I '$(shell $(COQBIN)coqc -where)/plugins/micromega' -R . SMTCoq -COQMF_COQLIBS_NOML = -R . SMTCoq - -############################################################################### -# # -# Coq configuration. # -# # -############################################################################### - -COQMF_LOCAL=1 -COQMF_COQLIB=/home/artemis/Autres/coq-8.7.2// -COQMF_DOCDIR=/home/artemis/Autres/coq-8.7.2/doc/ -COQMF_OCAMLFIND=/usr/bin/ocamlfind -COQMF_CAMLP4=camlp5 -COQMF_CAMLP4O=/usr/bin/camlp5o -COQMF_CAMLP4BIN=/usr/bin/ -COQMF_CAMLP4LIB=/usr/lib/ocaml/camlp5 -COQMF_CAMLP4OPTIONS=-loc loc -COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50 -safe-string -COQMF_HASNATDYNLINK=true -COQMF_COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml -COQMF_WINDRIVE=/home/artemis/Autres/coq-8.7.2 - -############################################################################### -# # -# Extra variables. # -# # -############################################################################### - -CAMLLEX = $(CAMLBIN)ocamllex -CAMLYACC = $(CAMLBIN)ocamlyacc -COQMF_OTHERFLAGS = -COQMF_INSTALLCOQDOCROOT = SMTCoq - -############################################################################### -# # -# Extra targets. (-extra and -extra-phony, DEPRECATED) # -# # -############################################################################### - -post-all:: - $(MAKE) -f $(SELF) test -clean:: - rm -f test -test : - cd ../unit-tests; make - -post-all:: - $(MAKE) -f $(SELF) ztest -clean:: - rm -f ztest -ztest : - cd ../unit-tests; make zchaff - -post-all:: - $(MAKE) -f $(SELF) vtest -clean:: - rm -f vtest -vtest : - cd ../unit-tests; make verit - -post-all:: - $(MAKE) -f $(SELF) lfsctest -clean:: - rm -f lfsctest -lfsctest : - cd ../unit-tests; make lfsc - -%.ml : %.mll - $(CAMLLEX) $< - -%.ml %.mli : %.mly - $(CAMLYACC) $< - -.PHONY: smtcoq_plugin.mlpack.d -smtcoq_plugin.mlpack.d : verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml - - |