products/sources/formale Sprachen/Coq/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: SML

Original von: Coq©
##########################################################################
##         #   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)         ##
##########################################################################


# Makefile for Coq
#
# To be used with GNU Make >= 3.81.
#
# This Makefile is now separated into Makefile.{common,build,doc}.
# You won't find Makefiles in sub-directories and this is done on purpose.
# If you are not yet convinced of the advantages of a single Makefile, please
# read
#    http://aegis.sourceforge.net/auug97.pdf
# before complaining.
#
# When you are working in a subdir, you can compile without moving to the
# upper directory using "make -C ..", and the output is still understood
# by Emacs' next-error.
#
# Specific command-line options to this Makefile:
#
# make VERBOSE=1           # restore the raw echoing of commands
# make NO_RECALC_DEPS=1    # avoid recomputing dependencies
#
# Nota: the 1 above can be replaced by any non-empty value
#
# ----------------------------------------------------------------------
# See dev/doc/build-system*.txt for more details/FAQ about this Makefile
# ----------------------------------------------------------------------


###########################################################################
# File lists
###########################################################################

# NB: due to limitations in Win32, please refrain using 'export' too much
# to communicate between make sub-calls (in Win32, 8kb max per env variable,
# 32kb total)

# !! Before using FIND_SKIP_DIRS, please read how you should in the !!
# !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt         !!
FIND_SKIP_DIRS:='(' \
  -name '{arch}' -o \
  -name '.svn' -o \
  -name '_darcs' -o \
  -name '.git' -o \
  -name '.bzr' -o \
  -name 'debian' -o \
  -name "$${GIT_DIR}" -o \
  -name '_build' -o \
  -name '_build_ci' -o \
  -name '_install_ci' -o \
  -name 'gramlib' -o \
  -name 'user-contrib' -o \
  -name 'test-suite' -o \
  -name '.opamcache' -o \
  -name '.coq-native' -o \
  -name 'plugin_tutorial' \
')' -prune -o

define find
 $(shell find . $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||')
endef

define findindir
 $(shell find $(1) $(FIND_SKIP_DIRS) '(' -name $(2) ')' -print | sed 's|^\./||')
endef

## Files in the source tree

# instead of using "export FOO" do "COQ_EXPORTED += FOO"
# this makes it possible to clean up the environment in the subcall
COQ_EXPORTED := COQ_EXPORTED

LEXFILES := $(call find, '*.mll')
YACCFILES := $(call find, '*.mly')
MLLIBFILES := $(call find, '*.mllib')
MLPACKFILES := $(call find, '*.mlpack')
MLGFILES := $(call find, '*.mlg')
CFILES := $(call findindir, 'kernel/byterun', '*.c')
COQ_EXPORTED +=MLLIBFILES MLPACKFILES MLGFILES CFILES

# NB our find wrapper ignores the test suite
MERLININFILES := $(call find, '.merlin.in') test-suite/unit-tests/.merlin.in
MERLINFILES := $(MERLININFILES:.in=)
COQ_EXPORTED += MERLINFILES

# NB: The lists of currently existing .ml and .mli files will change
# before and after a build or a make clean. Hence we do not export
# these variables, but cleaned-up versions (see below MLFILES and co)

EXISTINGML := $(call find, '*.ml')
EXISTINGMLI := $(call find, '*.mli')

## Files that will be generated

# GRAMFILES must be in linking order
GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Grammar)
GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES))
GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES))
GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES?

GENMLGFILES:= $(MLGFILES:.mlg=.ml)
GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml
GENMLIFILES:=$(GRAMMLIFILES)
GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h
GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
COQ_EXPORTED += GRAMFILES GRAMMLFILES GRAMMLIFILES GENMLFILES GENHFILES GENFILES

## More complex file lists

MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML))
MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
COQ_EXPORTED += MLSTATICFILES MLIFILES

export $(COQ_EXPORTED)

include Makefile.common

###########################################################################
# Starting rules
###########################################################################

NOARG: world

.PHONY: NOARG help noconfig submake camldevfiles

help:
 @echo "Please use either:"
 @echo "   ./configure"
 @echo "   make world"
 @echo "   make install"
 @echo "   make clean"
 @echo "or make archclean"
 @echo "For make to be verbose, add VERBOSE=1"
 @echo
 @echo "Bytecode compilation is now a separate target:"
 @echo "   make byte"
 @echo "   make install-byte"
 @echo "Please do not mix bytecode and native targets in the same make -j"

UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?')
ifdef UNSAVED_FILES
$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; \
cancel them or save before proceeding. Or your editor crashed. \
Then, you may want to consider whether you want to restore the autosaves)
#If you try to simply remove this explicit test, the compilation may
#fail later. In particular, if a .#*.v file exists, coqdep fails to
#run.
endif

# Apart from clean and a few misc files, everything will be done in a
# sub-call to make on Makefile.build. This way, we avoid doing here
# the -include of .d : since they trigger some compilations, we do not
# want them for a mere clean. Moreover, we regroup this sub-call in a
# common target named 'submake'. This way, multiple user-given goals
# (cf the MAKECMDGOALS variable) won't trigger multiple (possibly
# parallel) make sub-calls

ifdef COQ_CONFIGURED
%:: submake ;
else
%:: noconfig ;
endif

MAKE_OPTS := --warn-undefined-variable --no-builtin-rules

bin:
 mkdir bin

submake: alienclean camldevfiles | bin
 $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS)

noconfig:
 @echo "Please run ./configure first" >&2; exit 1

# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles

Makefile $(wildcard Makefile.*) config/Makefile : ;

###########################################################################
# OCaml dev files
###########################################################################
camldevfiles: $(MERLINFILES) META.coq

# prevent submake dependency
META.coq.in $(MERLININFILES): ;

.merlin: .merlin.in
 cp -a "$<" "$@"

%/.merlin: %/.merlin.in
 cp -a "$<" "$@"

META.coq: META.coq.in
 cp -a "$<" "$@"

###########################################################################
# Cleaning
###########################################################################

.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean plugin-tutorialclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean

clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean

cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean

objclean: archclean indepclean

.PHONY: gramlibclean
gramlibclean:
 rm -rf gramlib/.pack/

cruftclean: mlgclean
 find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} +
 rm -f gmon.out core

camldevfilesclean:
 rm -f $(MERLINFILES) META.coq

indepclean:
 rm -f $(GENFILES)
 rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE)
 find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -exec rm -f {} +
 rm -f */*.pp[iox] plugins/*/*.pp[iox]
 rm -rf $(SOURCEDOCDIR)
 rm -f toplevel/mltop.byteml toplevel/mltop.optml
 rm -f glob.dump
 rm -f config/revision.ml revision
 rm -f plugins/micromega/.micromega.ml.generated
 $(MAKE) -C test-suite clean

docclean:
 rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \
 doc/*/*.idx doc/*/*~ doc/*/*.ilg doc/*/*.ind doc/*/*.dvi.gz doc/*/*.ps.gz doc/*/*.pdf.gz\
 doc/*/*.???idx doc/*/*.???ind doc/*/*.v.tex doc/*/*.atoc doc/*/*.lof\
 doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \
 doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html
 rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \
   doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \
   doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex
 rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t
 rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html
 rm -f doc/common/version.tex
 rm -f doc/coq.tex
 rm -rf doc/sphinx/_build

archclean: clean-ide optclean voclean plugin-tutorialclean
 rm -rf _build
 rm -f $(ALLSTDLIB).*

optclean:
 rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT)
 rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT)
 find . \( -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' \) -exec rm -f {} +

clean-ide:
 rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE)
 rm -f ide/input_method_lexer.ml
 rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
 rm -f ide/utf8_convert.ml
 rm -f ide/default.bindings
 rm -rf $(COQIDEAPP)

mlgclean:
 rm -f $(GENMLGFILES)

depclean:
 find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} +

cacheclean:
 find theories plugins test-suite -name '.*.aux' -exec rm -f {} +

cleanconfig:
 rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist

distclean: clean cleanconfig cacheclean timingclean

voclean:
 find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.glob' -o -name "*.cmxs" \
 -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} +
 find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} +

timingclean:
 find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \
   -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" \
   -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \
   -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} +

plugin-tutorialclean:
 +$(MAKE) -C $(PLUGINTUTO) clean

# Ensure that every compiled file around has a known source file.
# This should help preventing weird compilation failures caused by leftover
# compiled files after deleting or moving some source files.

EXISTINGVO:=$(call find, '*.vo')
KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v'))
ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO))

EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa')
KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \
 $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp))
KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \
 $(MLIFILES:.mli=.cmi) \
 gramlib/.pack/gramlib.cma gramlib/.pack/gramlib.cmxa $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma
ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS))

alienclean:
 rm -f $(ALIENOBJS) $(ALIENVO)

###########################################################################
# Continuous Intregration Tests
###########################################################################
include Makefile.ci

###########################################################################
# Emacs tags
###########################################################################

.PHONY: tags printenv

tags:
 echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \
 etags --language=none\
       "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
       "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
       "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
       "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
              "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
       "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
       "--regex=/module[ \t]+\([^ \t]+\)/\1/"
 echo $(MLGFILES) | sort -r | xargs \
 etags --append --language=none\
       "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"

checker-tags:
 echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \
 etags --language=none\
       "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
       "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
       "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
       "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
              "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
       "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
       "--regex=/module[ \t]+\([^ \t]+\)/\1/"
 echo $(MLGFILES) | sort -r | xargs \
 etags --append --language=none\
       "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"

# Useful to check that the exported variables are within the win32 limits

printenv:
 @env
 @echo
 @echo -n "Maxsize (win32 limit is 8k) : "
 @env | wc -L
 @echo -n "Total (win32 limit is 32k) : "
 @env | wc -m

¤ Dauer der Verarbeitung: 0.25 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff