Closed msprotz closed 5 years ago
Two thoughts:
Two good suggestions. For 2., I indeed see two invocations trying to build fstarlib.cmxa in the log (fstarlib.a is a byproduct of the construction of fstarlib.cmxa, and ocamlopt writes out both).
The second invocation ends like this:
make[5]: 'FStar_All.o' is up to date.
make[5]: Leaving directory '/cygdrive/c/Build/Agent/_work/1/s/ulib/ml'
ocamlopt -a prims.cmx FStar_Mul.cmx FStar_Float.cmx FStar_Char.cmx FStar_Int8.cmx FStar_UInt8.cmx FStar_Int16.cmx FStar_UInt16.cmx FStar_Int32.cmx FStar_UInt32.cmx FStar_Int64.cmx FStar_UInt64.cmx FStar_UInt128.cmx FStar_Int_Cast.cmx FStar_BaseTypes.cmx FStar_IO.cmx FStar_Heap.cmx FStar_List.cmx FStar_Option.cmx FStar_String.cmx FStar_Set.cmx FStar_Buffer.cmx FStar_CommonST.cmx FStar_ST.cmx FStar_All.cmx -o fstarlib.cmxa
The Makefile correctly declines to rebuild the intermediary .o files (they've been built already) but insists on rebuilding the cmxa...
Seems like some unwanted concurrency if two recursive invocations of make are trying to build the same artifact at the same time.
That sounds like the problem. One more reason to switch to Scons, and have it oversee the entire build rather than depending on multiple invocations of make.
Haven't seen this for a long time since we switched to Azure DevOps.
We're seeing strange errors about "Device or resource busy".
Here's a build that exhibited the problem:
https://raw.githubusercontent.com/project-everest/ci-logs/master/fstar-ci-5ff3bc6e-4025.all
Probably difficult to debug.