OMakefile

OMakeVersion(0.9.8.5)

#
# OCaml
#
OCAMLFLAGS += -safe-string

#
# Locations of the source tree.
#
LIB      = $(dir lib)
BIN      = $(dir bin)
EXPORT   = $(dir export)
MK       = $(dir mk)
ROOT     = $(dir .)
EDITOR   = $(dir editor/ml)
MP_ROOT  = $(ROOT)

SHARED_MODE = false

include mk/load_config
include OMakefile_common

$(BIN):
    mkdir -p $@

$(LIB):
    mkdir -p $@

########################################################################
# Directories needing only the standard config
#
.SUBDIRS: clib util

########################################################################
# For the rest of MetaPRL, use our custom scanner.
#
OCAMLDEP_MODULES_ENABLED = false

OCAMLDEP = $(file $(BIN)/ocamldep$(EXE))

OCAMLDEPFLAGS += -omake

.SCANNER: scan-ocaml-%.mli: %.mli $(OCAMLDEP) OCamlGeneratedFilesTarget
.SCANNER: scan-ocaml-%.ml: %.ml $(OCAMLDEP) OCamlGeneratedFilesTarget :exists: %.mli

#
# Libmojave is using our custom scanner, but otherwise config is normal
#
.SUBDIRS: libmojave

OCAMLINCLUDES += $(dir libmojave/stdlib libmojave/util libmojave/unix)

########################################################################
# Refiner building
#

# Macro preprocess
MACROPP = $(file $(LIB)/macropp$(EXE))
MACROPRINT = $(file $(LIB)/macroprint$(EXE))

#
# For the refiner and mllib directories,
# add a dependency on the macro processor.
#
section
    # Add the extra dependency
    %.cmi: $(MACROPP)
    %.cmo: $(MACROPP)
    %.cmx: $(MACROPP)

    MACROPPOPTS =
    OCAMLPPFLAGS = -pp $`(quote-argv $(MACROPP) $(MACROPPOPTS))

    %.p4: %.ml $(MACROPRINT)
        $(MACROPRINT) $(MACROPPOPTS) $< > $@

    %.p4i: %.mli $(MACROPRINT)
        $(MACROPRINT) $(MACROPPOPTS) $< > $@

    # These directories use the macro preprocessor
    .SUBDIRS: mllib

    OCAMLINCLUDES += $(dir mllib)

    .SUBDIRS: refiner

OCAMLINCLUDES += $(dir mllib)

.SUBDIRS: proxyedit

OCAMLINCLUDES += $(dir refiner/refsig refiner/refbase refiner/refiner refiner/reflib $(CAMLP5LIB))

########################################################################
# Generic directories with no special options
#
.SUBDIRS: library debug $(ENSEMBLE_DIR) tactics/proof

# Add camlp5 library to include path
OCAMLINCLUDES += $(dir library tactics/proof)

.SUBDIRS: filter

OCAMLINCLUDES += $(dir filter/base filter/filter)

########################################################################
# Theory building
#

#
# Capture the current environment so that some files can use it
# in some places.
#
STANDARD_BUILD_ENV = $(export .RULE)

#
# Include the support directories
#
SUPPORT = $(dir support)
SUPPORT_DIRS = $(dir support/display support/shell support/tactics support/doc)
OCAMLINCLUDES[] += $(SUPPORT_DIRS)

#
# Config for building theories
#
include OMakefile_theories

#
# Also build documentation
#
.SUBDIRS: doc

#
# Additional theories
#
section
   OCAML_LIB_FLAGS += -linkall
   THEORYNAME = support
   THEORYDESCR = MetaPRL Internal "Helper" Modules
   .SUBDIRS: $(SUPPORT) editor/ml

########################################################################
# Check-status
#
.PHONY: check-status core-incompletes

if $(NATIVE_ENABLED)
   check-status core-incompletes: util/check-status util/check-status.sh $(MP_PREREQS) support/editor/svnversion.txt

   check-status:
      util/check-status nomake

   core-incompletes:
      util/check-status nomake core

else
    err[] =
        The check-status and core-incompletes targets expect MetaPRL to be compiled
        to native code.
        $(EMPTY)
        Set COMPILATION_MODE to native or both in mk/config, if you need check-status
        $(EMPTY)
    check-status core-incompletes:
        ConfMsgError($(err))

########################################################################
# Installation
#

#
# Extra files to install in lib/mk/
#
ExportInstallDir(mk)
ExportSubInstallNamed(mk, OMakefile_editor, editor/ml/OMakefile)
ExportSubInstall(mk, OMakefile_common OMakefile_theories mk/prlcomp mk/config mk/ro_config mk/defaults)

#
# Generate the OMakeroot file for read-only clients
#
GENROOT = mk/gen_omakeroot

include $(GENROOT)

$(EXPORT)/mk/OMakeroot: $(GENROOT) $(EXPORT)/mk
    fprint($@, $(OMakeroot))

$(EXPORT)/mk/OCaml_version: $(where ocamlc) $(EXPORT)/mk
    fprint($@, $"CAML_VERSIONS = ")
    ocamlc -version >> $@

$(MPINSTALL): $(EXPORT)/mk/OMakeroot $(EXPORT)/mk/OCaml_version

#
# Install everything
#
install: $(MPINSTALL)
    mkdir -p $(INSTALL_DIR)
    /bin/cp -L -r --remove-destination $(LIB) $(INSTALL_DIR)
    /bin/cp -L -r --remove-destination $(BIN) $(INSTALL_DIR)
    /bin/cp -L -r --remove-destination $(EXPORT)/mk $(INSTALL_DIR)
    /bin/cp -L -r --remove-destination $(EXPORT)/theories $(INSTALL_DIR)