search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.68k stars 231 forks source link

Sanitization/hygiene too aggressive or our regressions too dirty? #1035

Open catalin-hritcu opened 7 years ago

catalin-hritcu commented 7 years ago

Now simply running our regressions causes a "hygiene violations" error when trying to make ocaml-fstar-ocaml afterwards:

SANITIZE: a total of 80 files that should probably not be in your source tree
  has been found. A script shell file
  "/home/hritcu/Projects/fstar/pub/src/ocaml-output/_build/sanitize.sh" is
  being created. Check this script and run it to remove unwanted files or use
  other options (such as defining hygiene exceptions or using the -no-hygiene
  option).
IMPORTANT: I cannot work with leftover compiled files.
ERROR: Leftover object files:
  File FStar_Mul.o in ulib/ml has suffix .o
  File FStar_UInt16.o in ulib/ml has suffix .o
  File FStar_Set.o in ulib/ml has suffix .o
  File prims.o in ulib/ml has suffix .o
  File FStar_Int16.o in ulib/ml has suffix .o
  File FStar_Char.o in ulib/ml has suffix .o
  File FStar_Int8.o in ulib/ml has suffix .o
  File FStar_ST.o in ulib/ml has suffix .o
  File FStar_List.o in ulib/ml has suffix .o
  File FStar_Int_Cast.o in ulib/ml has suffix .o
  File FStar_UInt32.o in ulib/ml has suffix .o
  File FStar_UInt8.o in ulib/ml has suffix .o
  File FStar_Int32.o in ulib/ml has suffix .o
  File FStar_Option.o in ulib/ml has suffix .o
  File FStar_Float.o in ulib/ml has suffix .o
  File FStar_Buffer.o in ulib/ml has suffix .o
  File FStar_CommonST.o in ulib/ml has suffix .o
  File FStar_String.o in ulib/ml has suffix .o
  File FStar_BaseTypes.o in ulib/ml has suffix .o
  File FStar_Int64.o in ulib/ml has suffix .o
  File FStar_UInt64.o in ulib/ml has suffix .o
  File FStar_Heap.o in ulib/ml has suffix .o
  File FStar_List_Tot_Base.o in ulib/ml has suffix .o
  File FStar_IO.o in ulib/ml has suffix .o
  File FStar_All.o in ulib/ml has suffix .o
  File FStar_UInt128.o in ulib/ml has suffix .o
  File fstarlib.a in ulib/ml has suffix .a
ERROR: Leftover OCaml compilation files:
  File FStar_UInt32.cmi in ulib/ml has suffix .cmi
  File FStar_Heap.cmi in ulib/ml has suffix .cmi
  File FStar_List_Tot_Base.cmi in ulib/ml has suffix .cmi
  File FStar_Set.cmi in ulib/ml has suffix .cmi
  File FStar_CommonST.cmi in ulib/ml has suffix .cmi
  File FStar_UInt8.cmi in ulib/ml has suffix .cmi
  File FStar_UInt64.cmi in ulib/ml has suffix .cmi
  File FStar_All.cmi in ulib/ml has suffix .cmi
  File FStar_UInt16.cmi in ulib/ml has suffix .cmi
  File FStar_List.cmi in ulib/ml has suffix .cmi
  File FStar_BaseTypes.cmi in ulib/ml has suffix .cmi
  File FStar_Mul.cmi in ulib/ml has suffix .cmi
  File FStar_String.cmi in ulib/ml has suffix .cmi
  File FStar_UInt128.cmi in ulib/ml has suffix .cmi
  File FStar_Int8.cmi in ulib/ml has suffix .cmi
  File FStar_IO.cmi in ulib/ml has suffix .cmi
  File FStar_Int64.cmi in ulib/ml has suffix .cmi
  File prims.cmi in ulib/ml has suffix .cmi
  File FStar_Char.cmi in ulib/ml has suffix .cmi
  File FStar_ST.cmi in ulib/ml has suffix .cmi
  File FStar_Int32.cmi in ulib/ml has suffix .cmi
  File FStar_Int16.cmi in ulib/ml has suffix .cmi
  File FStar_Int_Cast.cmi in ulib/ml has suffix .cmi
  File FStar_Option.cmi in ulib/ml has suffix .cmi
  File FStar_Float.cmi in ulib/ml has suffix .cmi
  File FStar_Buffer.cmi in ulib/ml has suffix .cmi
  File FStar_UInt16.cmx in ulib/ml has suffix .cmx
  File FStar_UInt128.cmx in ulib/ml has suffix .cmx
  File FStar_Int16.cmx in ulib/ml has suffix .cmx
  File FStar_Heap.cmx in ulib/ml has suffix .cmx
  File FStar_BaseTypes.cmx in ulib/ml has suffix .cmx
  File FStar_All.cmx in ulib/ml has suffix .cmx
  File FStar_Int_Cast.cmx in ulib/ml has suffix .cmx
  File FStar_String.cmx in ulib/ml has suffix .cmx
  File FStar_Mul.cmx in ulib/ml has suffix .cmx
  File FStar_Option.cmx in ulib/ml has suffix .cmx
  File FStar_Int32.cmx in ulib/ml has suffix .cmx
  File FStar_List.cmx in ulib/ml has suffix .cmx
  File FStar_Float.cmx in ulib/ml has suffix .cmx
  File FStar_IO.cmx in ulib/ml has suffix .cmx
  File FStar_List_Tot_Base.cmx in ulib/ml has suffix .cmx
  File prims.cmx in ulib/ml has suffix .cmx
  File FStar_CommonST.cmx in ulib/ml has suffix .cmx
  File FStar_UInt8.cmx in ulib/ml has suffix .cmx
  File FStar_Char.cmx in ulib/ml has suffix .cmx
  File FStar_ST.cmx in ulib/ml has suffix .cmx
  File FStar_UInt64.cmx in ulib/ml has suffix .cmx
  File FStar_Set.cmx in ulib/ml has suffix .cmx
  File FStar_Int64.cmx in ulib/ml has suffix .cmx
  File FStar_UInt32.cmx in ulib/ml has suffix .cmx
  File FStar_Buffer.cmx in ulib/ml has suffix .cmx
  File FStar_Int8.cmx in ulib/ml has suffix .cmx
  File fstarlib.cmxa in ulib/ml has suffix .cmxa
Exiting due to hygiene violations.

The Makefiles for our regressions are full of $(MAKE) -C $(ULIB_ML) which creates these, including our hello world example, tutorial, etc:

[hritcu@resurrected pub]$ grep -R 'ULIB_ML'                                                                            (git)-[master] 
examples/printf/Makefile:   $(MAKE) -C $(ULIB_ML)
examples/low-level/old/ulib/Makefile:OCAMLOPT := $(OCAMLOPT) -I $(ULIB_ML)/native_int
examples/low-level/old/ulib/hyperstack/Makefile:OCAMLOPT := $(OCAMLOPT) -I $(ULIB_ML)/native_int
examples/dm4free/old/Makefile:  $(MAKE) -C $(ULIB_ML)
examples/algorithms/Makefile:   $(MAKE) -C $(ULIB_ML)
examples/algorithms/Makefile:   $(MAKE) -C $(ULIB_ML)
examples/algorithms/Makefile:   $(OCAMLC) -I out $(ULIB_ML)/prims.ml out/FStar_List_Tot_Base.ml out/Huffman.ml -o Huffman.exe
examples/algorithms/Makefile:   utop -I out -I $(ULIB_ML) Huffman.repl
examples/bug-reports/Makefile:  $(MAKE) -C $(ULIB_ML)
examples/hello/Makefile:    $(MAKE) -C $(ULIB_ML)
examples/hello/Makefile:    $(MAKE) -C $(ULIB_ML) PRIMS_DIR=native_int
examples/hello/Makefile:        # CH: reference to $(ULIB_ML)/native_int is now bogus, there is no such thing
examples/hello/Makefile:    $(OCAMLOPT) -I $(ULIB_ML)/native_int -I out/ out/FStar_Seq.ml out/TestSeq.ml -o testseq.exe
examples/hello/Makefile:    make -C $(ULIB_ML) clean
ulib/ml/Makefile.include:ULIB_ML=$(FSTAR_HOME)/ulib/ml
ulib/ml/Makefile.include:     OCAML_DEFAULT_FLAGS=$(ULIB_ML)/fstarlib.cmxa -I $(ULIB_ML)/extracted -I $(ULIB_ML)/hyperstack -I $(ULIB_ML)
ulib/ml/Makefile.include:     OCAML_DEFAULT_FLAGS=$(ULIB_ML)/fstarlib.cmxa -I $(ULIB_ML)/extracted -I $(ULIB_ML)
ulib/ml/Makefile.include:OCAMLC_=ocamlfind c -package batteries,stdint,zarith -linkpkg -g -I $(ULIB_ML)

So is our sanitization/hygiene too aggressive or are our our regressions too dirty? (Either way, something needs fixing.)

msprotz commented 7 years ago

It's an artefact of VSTS not cleaning the build directory (the idea being that you should be able to do an incremental build).

The solution would be to run make -C ../../ulib/ml clean in ocaml-output first thing.