Skip to content
Permalink
Browse files

Revert "wip silent makefile??"

This reverts commit 3e55510.
  • Loading branch information
mtzguido committed Nov 5, 2019
1 parent 0c9b5a5 commit 63ddfcd8ac350a3d350996d7c1825c4a6c227636
Showing with 88 additions and 108 deletions.
  1. +16 −18 Makefile
  2. +10 −14 examples/Makefile.common
  3. +1 −1 examples/Makefile.include
  4. +1 −1 src/Makefile
  5. +9 −12 src/Makefile.boot
  6. +0 −6 src/Makefile.common
  7. +0 −1 src/Makefile.config
  8. +51 −55 src/ocaml-output/Makefile
@@ -1,47 +1,45 @@
.PHONY: all package clean 0 1 2 3 hints

include src/Makefile.common

all:
$(Q)$(MAKE) -C src/ocaml-output
$(Q)$(MAKE) -C ulib
$(Q)$(MAKE) -C ulib/ml
$(MAKE) -C src/ocaml-output
$(MAKE) -C ulib
$(MAKE) -C ulib/ml

package:
$(Q)git clean -ffdx .
$(Q)$(MAKE) -C src/ocaml-output package
git clean -ffdx .
$(MAKE) -C src/ocaml-output package

clean:
$(Q)$(MAKE) -C ulib clean
$(Q)$(MAKE) -C src/ocaml-output clean
$(MAKE) -C ulib clean
$(MAKE) -C src/ocaml-output clean

# Shortcuts for developers

# Build the F# version
0:
$(Q)$(MAKE) -C src/
$(MAKE) -C src/

# Build the OCaml snapshot. NOTE: This will not build the standard library,
# nor tests, and native tactics will not run
1:
$(Q)$(MAKE) -C src/ocaml-output ../../bin/fstar.exe
$(MAKE) -C src/ocaml-output ../../bin/fstar.exe

# Bootstrap just the compiler, not the library and tests;
# fastest way to incrementally build a patch to the compiler
boot:
$(Q)$(MAKE) -C src/ ocaml
$(Q)$(MAKE) -C src/ocaml-output ../../bin/fstar.exe
$(MAKE) -C src/ ocaml
$(MAKE) -C src/ocaml-output ../../bin/fstar.exe

# Generate a new OCaml snapshot
2:
$(Q)$(MAKE) -C src fstar-ocaml
$(MAKE) -C src fstar-ocaml

# Build the snapshot and then regen, i.e. 1 + 2
3:
$(Q)$(MAKE) -C src ocaml-fstar-ocaml
$(MAKE) -C src ocaml-fstar-ocaml

# Regenerate all hints for the standard library and regression test suite
hints:
$(Q)OTHERFLAGS=--record_hints $(MAKE) -C ulib/
$(Q)OTHERFLAGS=--record_hints $(MAKE) -C ulib/ml
$(Q)OTHERFLAGS=--record_hints $(MAKE) -C src/ uregressions
OTHERFLAGS=--record_hints $(MAKE) -C ulib/
OTHERFLAGS=--record_hints $(MAKE) -C ulib/ml
OTHERFLAGS=--record_hints $(MAKE) -C src/ uregressions
@@ -1,7 +1,6 @@
FSTAR_HOME?=..
include $(FSTAR_HOME)/ulib/gmake/z3.mk
include $(FSTAR_HOME)/ulib/gmake/fstar.mk
include $(FSTAR_HOME)/src/Makefile.common
FSTAR=$(FSTAR_HOME)/bin/fstar.exe

#################################################################################
@@ -34,12 +33,11 @@ OTHERFLAGS += --use_extracted_interfaces true --use_hints
# YOU SHOULDN'T NEED TO TOUCH THE REST
################################################################################

MY_FSTAR=$(Q)$(FSTAR) $(SIL) \
--cache_checked_modules \
--odir $(OUTPUT_DIRECTORY) \
--cache_dir $(CACHE_DIR) \
$(addprefix --include , $(INCLUDE_PATHS)) \
$(OTHERFLAGS)
MY_FSTAR=$(FSTAR) --cache_checked_modules \
--odir $(OUTPUT_DIRECTORY) \
--cache_dir $(CACHE_DIR) \
$(addprefix --include , $(INCLUDE_PATHS)) \
$(OTHERFLAGS)

#--------------------------------------------------------------------------------
# Default target: verify all FSTAR_FILES
@@ -50,7 +48,7 @@ MY_FSTAR=$(Q)$(FSTAR) $(SIL) \
# since we rely on the dependences it computes in other rules
#--------------------------------------------------------------------------------
.depend: $(FSTAR_FILES)
$(Q)$(MY_FSTAR) --dep full $(FSTAR_FILES) > .depend
$(MY_FSTAR) --dep full $(FSTAR_FILES) > .depend

depend: .depend

@@ -59,15 +57,13 @@ include .depend

# a.fst.checked is the binary, checked version of a.fst
%.fst.checked:
@echo "[CHECK $(basename $(notdir $@))]"
$(Q)$(MY_FSTAR) $<
@touch -c $@
$(MY_FSTAR) $<
touch -c $@

# a.fsti.checked is the binary, checked version of a.fsti
%.fsti.checked:
@echo "[CHECK $(basename $(notdir $@))]"
$(Q)$(MY_FSTAR) $<
@touch -c $@
$(MY_FSTAR) $<
touch -c $@

clean:
rm -rf $(CACHE_DIR)
@@ -17,7 +17,7 @@ endif
# we ignore the return result in benchmark runs because we can have micro-benchmarks which
# produce error asserts when executed with '--admit_smt_queries true'
%.uver: %.fst
$(Q)$(BENCHMARK_PRE) $(FSTAR) --use_extracted_interfaces true $^
$(BENCHMARK_PRE) $(FSTAR) --use_extracted_interfaces true $^

%.fail-uver: %.fst
(! $(FSTAR) $^ >/dev/null 2>&1) || (echo "NEGATIVE TEST FAILED ($@)!" ; false)
@@ -120,7 +120,7 @@ clean_boot:
# And ocaml-output/Makefile, to actually build the compiler in OCaml
# --------------------------------------------------------------------------------
ocaml: boot
$(Q)+$(MAKE) -f Makefile.boot all-ml
+$(MAKE) -f Makefile.boot all-ml

boot-ocaml:
+$(MAKE) -C ocaml-output all
@@ -46,15 +46,13 @@ EXTRACT = $(addprefix --extract_module , $(EXTRACT_MODULES)) \
# ensures that if this rule is successful then %.checked.lax is more
# recent than its dependences.
%.checked.lax:
@echo "[CHECK $(basename $(notdir $@))]"
$(Q)$(FSTAR_C) $(SIL) $< --already_cached "* -$(basename $(notdir $<))"
$(Q)@touch $@
$(FSTAR_C) $< --already_cached "* -$(basename $(notdir $<))"
touch $@

# And then, in a separate invocation, from each .checked.lax we
# extract an .ml file
ocaml-output/%.ml:
@echo "[EXTRACT $(basename $(notdir $@))]"
$(Q)$(BENCHMARK_PRE) $(FSTAR_C) $(SIL) $(notdir $(subst .checked.lax,,$<)) \
$(BENCHMARK_PRE) $(FSTAR_C) $(notdir $(subst .checked.lax,,$<)) \
--codegen OCaml \
--extract_module $(basename $(notdir $(subst .checked.lax,,$<)))

@@ -71,13 +69,12 @@ ocaml-output/%.ml:
# the dependency analysis failed.

.depend:
@echo "[DEPEND]"
$(Q)$(FSTAR_C) $(SIL) --dep full \
fstar/FStar.Main.fs \
boot/FStar.Tests.Test.fst \
$(EXTRACT) > ._depend
$(Q)mv ._depend .depend
$(Q)mkdir -p $(CACHE_DIR)
$(FSTAR_C) --dep full \
fstar/FStar.Main.fs \
boot/FStar.Tests.Test.fst \
$(EXTRACT) > ._depend
mv ._depend .depend
mkdir -p $(CACHE_DIR)

depend: .depend

This file was deleted.

@@ -1,5 +1,4 @@
FSTAR_HOME=..
include Makefile.common
include $(FSTAR_HOME)/ulib/gmake/z3.mk # This pins $(Z3) ...
include $(FSTAR_HOME)/ulib/gmake/fstar.mk # and $(FSTAR) for all sub-make calls

@@ -6,8 +6,6 @@ else
HAS_VALID_MENHIR := 0
endif
include ../Makefile.common
MENHIR=menhir #--explain --infer -la 1 --table
OCAMLLEX=ocamllex
FSTAR_OCAMLBUILD_EXTRAS ?= -cflag -g
@@ -64,43 +62,42 @@ endif
# This is about the F# parser, which we sed-transform from the parse.mly
# obtained via the rule above.
../parser/parse.fsy: parse.mly
$(Q)echo "%{" > $@
$(Q)echo "#light \"off\"" >> $@
$(Q)echo "// (c) Microsoft Corporation. All rights reserved" >> $@
$(Q)echo "open Prims" >> $@
$(Q)echo "open FStar" >> $@
$(Q)echo "open FStar.Errors" >> $@
$(Q)echo "open FStar.List" >> $@
$(Q)echo "open FStar.Util" >> $@
$(Q)echo "open FStar.Range" >> $@
$(Q)echo "open FStar.Options" >> $@
$(Q)echo "open FStar.Parser.Const" >> $@
$(Q)echo "open FStar.Parser.AST" >> $@
$(Q)echo "open FStar.Parser.Util" >> $@
$(Q)echo "open FStar.Const" >> $@
$(Q)echo "open FStar.Ident" >> $@
$(Q)echo "open FStar.String" >> $@
echo "%{" > $@
echo "#light \"off\"" >> $@
echo "// (c) Microsoft Corporation. All rights reserved" >> $@
echo "open Prims" >> $@
echo "open FStar" >> $@
echo "open FStar.Errors" >> $@
echo "open FStar.List" >> $@
echo "open FStar.Util" >> $@
echo "open FStar.Range" >> $@
echo "open FStar.Options" >> $@
echo "open FStar.Parser.Const" >> $@
echo "open FStar.Parser.AST" >> $@
echo "open FStar.Parser.Util" >> $@
echo "open FStar.Const" >> $@
echo "open FStar.Ident" >> $@
echo "open FStar.String" >> $@
@# TODO : fsyacc seems to complain as soon as there is an arrow -> in a %type declaration...
$(Q)cat parse.mly | sed -e '/%{/d' \
cat parse.mly | sed -e '/%{/d' \
-e '/^open /d' \
-e '/%token/s/[a-zA-Z0-9_]*\.//g' \
-e '/%type/s/[a-zA-Z0-9_]*\.//g' \
-e '/%token.*->.*/d' \
-e '/%type.*->.*/d' \
| cat -s >> $@
| cat -s >> $@
# https://stackoverflow.com/questions/38294095/ocaml-how-to-solve-findlib-warnings-of-multiple-cmis
FSTAR_MAIN_NATIVE=_build/src/fstar/ml/main.native
$(FSTAR_MAIN_NATIVE): export OCAMLFIND_IGNORE_DUPS_IN = $(shell ocamlfind query compiler-libs)
$(FSTAR_MAIN_NATIVE): $(GENERATED_FILES)
@echo "[OCAMLBUILD]"
$(Q)$(OCAMLBUILD) $(notdir $(FSTAR_MAIN_NATIVE)) src/ocaml-output/FStar_Syntax_Syntax.inferred.mli
$(OCAMLBUILD) $(notdir $(FSTAR_MAIN_NATIVE)) src/ocaml-output/FStar_Syntax_Syntax.inferred.mli
../../bin/fstar.exe: $(FSTAR_MAIN_NATIVE)
$(Q)cp $^ $@
cp $^ $@
../../bin/fstar.ocaml: $(FSTAR_MAIN_NATIVE)
$(Q)cp $^ $@
cp $^ $@
install-compiler-lib: $(FSTAR_MAIN_NATIVE)
mkdir -p ../../bin/fstar-compiler-lib/
@@ -114,39 +111,38 @@ install-compiler-lib: $(FSTAR_MAIN_NATIVE)
FStar_Parser_Parse.ml: parse.mly
@# We are opening the same module twice but we need these modules
@# open for the definition of tokens
$(Q)echo "open Prims" > $@
$(Q)echo "open FStar_Errors" >> $@
$(Q)echo "open FStar_List" >> $@
$(Q)echo "open FStar_Util" >> $@
$(Q)echo "open FStar_Range" >> $@
$(Q)echo "open FStar_Options" >> $@
$(Q)echo "open FStar_Syntax_Syntax" >> $@
$(Q)echo "open FStar_Parser_Const" >> $@
$(Q)echo "open FStar_Syntax_Util" >> $@
$(Q)echo "open FStar_Parser_AST" >> $@
$(Q)echo "open FStar_Parser_Util" >> $@
$(Q)echo "open FStar_Const" >> $@
$(Q)echo "open FStar_Ident" >> $@
$(Q)echo "open FStar_String" >> $@
echo "open Prims" > $@
echo "open FStar_Errors" >> $@
echo "open FStar_List" >> $@
echo "open FStar_Util" >> $@
echo "open FStar_Range" >> $@
echo "open FStar_Options" >> $@
echo "open FStar_Syntax_Syntax" >> $@
echo "open FStar_Parser_Const" >> $@
echo "open FStar_Syntax_Util" >> $@
echo "open FStar_Parser_AST" >> $@
echo "open FStar_Parser_Util" >> $@
echo "open FStar_Const" >> $@
echo "open FStar_Ident" >> $@
echo "open FStar_String" >> $@
@# TODO: create a proper OCamlbuild rule for this production so that
@# OCamlbuild knows how to generate parse.mly first (possibly using
@# menhir) and removes the production as needed.
@echo "[OCAMLYACC]"
$(Q)ocamlyacc parse.mly 2> yac-log
$(Q)cat yac-log
ocamlyacc parse.mly 2> yac-log
cat yac-log
@if [ "0$$(grep "shift/reduce" yac-log | sed 's/^\([0-9]\+\).*/\1/')" -gt 6 ]; then \
@echo "shift-reduce conflicts have increased; please fix" && exit 255; \
echo "shift-reduce conflicts have increased; please fix" && exit 255; \
fi
@if grep -q "reduce/reduce" yac-log ; then \
@echo "A reduce-reduce conflict was introduced; please fix" && exit 255; \
echo "A reduce-reduce conflict was introduced; please fix" && exit 255; \
fi
$(Q)cat parse.ml >> $@
$(Q)rm parse.ml parse.mli
cat parse.ml >> $@
rm parse.ml parse.mli
../../bin/tests.exe: export OCAMLFIND_IGNORE_DUPS_IN = $(shell ocamlfind query compiler-libs)
../../bin/tests.exe: ../../bin/fstar.exe
$(Q)$(OCAMLBUILD) FStar_Tests_Main.native
$(Q)cp -f _build/src/tests/ml/FStar_Tests_Main.native $@
$(OCAMLBUILD) FStar_Tests_Main.native
cp -f _build/src/tests/ml/FStar_Tests_Main.native $@
# always bump version for a release; always bump it when recompiling so that one
# can easily help debugging
@@ -167,14 +163,14 @@ COMMITDATE = $(shell git log --pretty=format:%ci -n 1 2>/dev/null || echo unset)
.PHONY: FStar_Version.ml
FStar_Version.ml:
$(Q)echo 'open FStar_Util' > $@
$(Q)echo 'let dummy () = ();;' >> $@
$(Q)echo 'FStar_Options._version := "$(VERSION)";;' >> $@
$(Q)echo 'FStar_Options._platform := "$(PLATFORM)";;' >> $@
$(Q)echo 'FStar_Options._compiler := "$(COMPILER)";;' >> $@
@# We deliberately use commitdate instead of date, so that rebuilds are no-ops
$(Q)echo 'FStar_Options._date := "$(COMMITDATE)";;' >> $@
$(Q)echo 'FStar_Options._commit:= "$(COMMIT)";;' >> $@
echo 'open FStar_Util' > $@
echo 'let dummy () = ();;' >> $@
echo 'FStar_Options._version := "$(VERSION)";;' >> $@
echo 'FStar_Options._platform := "$(PLATFORM)";;' >> $@
echo 'FStar_Options._compiler := "$(COMPILER)";;' >> $@
# We deliberately use commitdate instead of date, so that rebuilds are no-ops
echo 'FStar_Options._date := "$(COMMITDATE)";;' >> $@
echo 'FStar_Options._commit:= "$(COMMIT)";;' >> $@
# ------------------------------------------------------------------------------

0 comments on commit 63ddfcd

Please sign in to comment.
You can’t perform that action at this time.