-
Notifications
You must be signed in to change notification settings - Fork 5
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #184 from mtzguido/stage
Removing the snapshot and staging the build
- Loading branch information
Showing
22 changed files
with
224 additions
and
28,822 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| *.ml | ||
| *.checked |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,92 @@ | ||
| # This makefile is included from several other makefiles in the tree. | ||
|
|
||
| MAKEFLAGS += --no-builtin-rules | ||
| Q?=@ | ||
| SIL?=--silent | ||
| RUNLIM= | ||
| ifneq ($(V),) | ||
| Q= | ||
| SIL= | ||
| else | ||
| MAKEFLAGS += -s | ||
| endif | ||
|
|
||
| define NO_RUNLIM_ERR | ||
| runlim not found: | ||
| To use RESOURCEMONITOR=1, the `runlim` tool must be installed and in your $$PATH. | ||
| It must also be a recent version supporting the `-p` option. | ||
| You can get it from: [https://github.com/arminbiere/runlim] | ||
| endef | ||
|
|
||
| define msg = | ||
| @printf " %-14s %s\n" $(1) $(2) | ||
| endef | ||
| define bold_msg = | ||
| @#-tput bold 2>/dev/null | ||
| @printf -- " %-15s" $(1) | ||
| @#-tput sgr0 2>/dev/null | ||
| @printf " %s\n" $(2) | ||
| endef | ||
|
|
||
| # Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with | ||
| # information about the time and space taken by each F* invocation. | ||
| ifneq ($(RESOURCEMONITOR),) | ||
| ifeq ($(shell which runlim),) | ||
| _ := $(error $(NO_RUNLIM_ERR))) | ||
| endif | ||
| ifneq ($(MONID),) | ||
| MONPREFIX=$(MONID). | ||
| endif | ||
| RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim | ||
| endif | ||
|
|
||
| # Ensure that any failing rule will not create its target file. | ||
| # In other words, make `make` less insane. | ||
| .DELETE_ON_ERROR: | ||
|
|
||
| .DEFAULT_GOAL:=__undef | ||
| .PHONY: __undef | ||
| __undef: | ||
| $(error "This makefile does not have a default goal") | ||
|
|
||
| # Check that a variable is defined. If not, abort with an (optional) error message. | ||
| need = \ | ||
| $(if $(value $(strip $1)),, \ | ||
| $(error Need a value for $(strip $1)$(if $2, ("$(strip $2)")))) | ||
|
|
||
| # Check that a variable is defined and pointing to an executable. | ||
| # Is there no negation in make...? | ||
| # Wew! this was interesting to write. Especially the override part. | ||
| need_exe = \ | ||
| $(if $(value $(strip $1)), \ | ||
| $(if $(wildcard $(value $(strip $1))), \ | ||
| $(if $(shell test -x $(value $(strip $1)) && echo 1), \ | ||
| $(eval override $(strip $1):=$(abspath $(value $(strip $1)))), \ | ||
| $(error $(strip $1) ("$(value $(strip $1))") is not executable)), \ | ||
| $(error $(strip $1) ("$(value $(strip $1))") does not exist (cwd = $(CURDIR)))), \ | ||
| $(error Need an executable for $(strip $1)$(if $2, ("$(strip $2)")))) \ | ||
|
|
||
| need_file = \ | ||
| $(if $(value $(strip $1)), \ | ||
| $(if $(wildcard $(value $(strip $1))), \ | ||
| $(if $(shell test -f $(value $(strip $1)) && echo 1), \ | ||
| $(eval override $(strip $1):=$(abspath $(value $(strip $1)))), \ | ||
| $(error $(strip $1) ("$(value $(strip $1))") is not executable)), \ | ||
| $(error $(strip $1) ("$(value $(strip $1))") does not exist (cwd = $(CURDIR)))), \ | ||
| $(error Need a file path for $(strip $1)$(if $2, ("$(strip $2)")))) \ | ||
|
|
||
| need_dir = \ | ||
| $(if $(value $(strip $1)), \ | ||
| $(if $(wildcard $(value $(strip $1))), \ | ||
| $(if $(shell test -d $(value $(strip $1)) && echo 1), \ | ||
| $(eval override $(strip $1):=$(abspath $(value $(strip $1)))), \ | ||
| $(error $(strip $1) ("$(value $(strip $1))") is not executable)), \ | ||
| $(error $(strip $1) ("$(value $(strip $1))") is not a directory (cwd = $(CURDIR)))), \ | ||
| $(error Need an *existing* directory path for $(strip $1)$(if $2, ("$(strip $2)")))) \ | ||
|
|
||
| need_dir_mk = \ | ||
| $(if $(value $(strip $1)), \ | ||
| $(if $(shell mkdir -p $(value $(strip $1)) && echo 1), \ | ||
| $(eval override $(strip $1):=$(abspath $(value $(strip $1)))), \ | ||
| $(error $(strip $1) ("$(value $(strip $1))") is not a directory (mkdir failed, cwd = $(CURDIR)))), \ | ||
| $(error Need a directory path for $(strip $1)$(if $2, ("$(strip $2)")))) \ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,69 @@ | ||
| include $(STEEL_HOME)/mk/common.mk | ||
|
|
||
| .DEFAULT_GOAL := ocaml | ||
| $(call need_exe, FSTAR_EXE, fstar.exe to be used) | ||
| $(call need_dir_mk, CACHE_DIR, directory for checked files) | ||
| $(call need_dir_mk, OUTPUT_DIR, directory for extracted OCaml files) | ||
| $(call need, CODEGEN, backend (OCaml / Plugin)) | ||
| $(call need_dir, SRC, source directory) | ||
| $(call need, TAG, a tag for the .depend; to prevent clashes. Sorry.) | ||
| $(call need, ROOTS, a list of roots for the dependency analysis) | ||
| # Optional: EXTRACT, DEPFLAGS | ||
|
|
||
| # This is to support both --lax and non --lax clients. | ||
| EXTENSION := $(if $(findstring --lax,$(FSTAR_OPTIONS)),.checked.lax,.checked) | ||
|
|
||
| .PHONY: clean | ||
| clean: | ||
| rm -rf $(CACHE_DIR) | ||
| rm -rf $(OUTPUT_DIR) | ||
|
|
||
| .PHONY: all | ||
| all: verify ocaml | ||
|
|
||
| .PHONY: ocaml | ||
| ocaml: all-ml | ||
|
|
||
| .PHONY: verify | ||
| verify: all-checked | ||
|
|
||
| FSTAR_OPTIONS += $(OTHERFLAGS) | ||
| FSTAR_OPTIONS += --odir "$(OUTPUT_DIR)" | ||
| FSTAR_OPTIONS += --cache_dir "$(CACHE_DIR)" | ||
| FSTAR_OPTIONS += --include "$(SRC)" | ||
| FSTAR_OPTIONS += --cache_checked_modules | ||
| FSTAR_OPTIONS += --warn_error -321 | ||
| FSTAR_OPTIONS += --compat_pre_typed_indexed_effects | ||
| ifeq ($(ADMIT),1) | ||
| FSTAR_OPTIONS += --admit_smt_queries true | ||
| endif | ||
|
|
||
| FSTAR = $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS) | ||
|
|
||
| %$(EXTENSION): FF=$(notdir $(subst $(EXTENSION),,$@)) | ||
| %$(EXTENSION): | ||
| $(call msg, "CHECK", $(FF)) | ||
| $(FSTAR) --already_cached '*' $< | ||
| @touch -c $@ ## SHOULD NOT BE NEEDED | ||
|
|
||
| %.ml: FF=$(notdir $(subst $(EXTENSION),,$<)) | ||
| %.ml: MM=$(basename $(FF)) | ||
| %.ml: LBL=$(notdir $@) | ||
| # ^ HACK we use notdir to get the module name since we need to pass in | ||
| # the fst (not the checked file), but we don't know where it is, so this | ||
| # is relying on F* looking in its include path. | ||
| %.ml: | ||
| $(call msg, "EXTRACT", $(LBL)) | ||
| $(FSTAR) $(FF) --already_cached '*' --codegen $(CODEGEN) --extract_module $(MM) | ||
| @touch -c $@ ## SHOULD NOT BE NEEDED | ||
|
|
||
| $(CACHE_DIR)/.depend$(TAG): | ||
| $(call msg, "DEPEND", $(SRC)) | ||
| $(FSTAR) --dep full $(ROOTS) $(EXTRACT) $(DEPFLAGS) --output_deps_to $@ | ||
| mkdir -p $(CACHE_DIR) | ||
|
|
||
| depend: $(CACHE_DIR)/.depend$(TAG) | ||
| include $(CACHE_DIR)/.depend$(TAG) | ||
|
|
||
| all-ml: $(ALL_ML_FILES) | ||
| all-checked: $(ALL_CHECKED_FILES) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.