FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Published 20 hours ago • verified publisher icon FStarLang

FStar does not compile on arm64, arm32 and ppc64

Open kit-ty-kate opened this issue 3 years ago • 6 comments

arm64 and ppc64:

#=== ERROR while compiling fstar.2021.06.06 ===================================#
# context              2.1.0 | linux/arm64 | ocaml-base-compiler.4.12.0 | pinned(https://github.com/FStarLang/FStar/archive/refs/tags/v2021.06.06.tar.gz)
# path                 ~/.opam/4.12/.opam-switch/build/fstar.2021.06.06
# command              ~/.opam/opam-init/hooks/sandbox.sh build make PREFIX=/home/opam/.opam/4.12 -j 31
# exit-code            2
# env-file             ~/.opam/log/fstar-12886-0599bd.env
# output-file          ~/.opam/log/fstar-12886-0599bd.out
### output ###
[...]
# ocamlfind ocamlopt -shared -linkall -thread -package batteries -package zarith -package ppx_deriving.std -package ppx_deriving_yojson -I ulib/tactics_ml ulib/tactics_ml/fstartaclib.cmxa -o ulib/tactics_ml/fstartaclib.cmxs
# [INSTALL   fstartaclib]
# make[3]: Leaving directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# make[2]: Leaving directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# make[1]: Leaving directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib/ml'
# make[1]: Entering directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# make FSTAR_HOME=.. -f Makefile.verify verify-core
# make[2]: Entering directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# ../bin/fstar.exe --warn_error @271   --use_hints --cache_dir .cache --hint_dir .cache --cache_checked_modules --odir _output --dep full  FStar.Pervasives.fst FStar.HyperStack.ST.fst FStar.Seq.Base.fst FStar.Int.Cast.fst FStar.Calc.fst FStar.List.Pure.Base.fst FStar.Reflection.Derived.fst FStar.PredicateExtensionality.fst FStar.Option.fst FStar.Math.Lib.fst FStar.Int32.fst FStar.Tactics.Print.fst FStar.List.Tot.fst FStar.Universe.fst FStar.BV.fst FStar.Math.Euclid.fst FStar.Int64.fst FStar.UInt8.fst FStar.Algebra.CommMonoid.fst FStar.SquashProperties.fst FStar.UInt32.fst FStar.Monotonic.DependentMap.fst FStar.IndefiniteDescription.fst FStar.Monotonic.Map.fst FStar.TSet.fst FStar.Util.fst FStar.UInt64.fst FStar.Heap.fst FStar.All.fst FStar.Squash.fst FStar.Modifies.fst FStar.Tactics.CanonCommMonoidSimple.fst FStar.ST.fst FStar.List.Tot.Properties.fst FStar.Reflection.Const.fst FStar.PropositionalExtensionality.fst FStar.BitVector.fst FStar.HyperStack.All.fst FStar.FunctionalExtensionality.fst FStar.Tactics.Canon.fst FStar.Seq.fst FStar.Seq.Sorted.fst FStar.Reflection.fst FStar.Math.Lemmas.fst FStar.Pervasives.Native.fst FStar.Int16.fst FStar.BigOps.fst FStar.MarkovsPrinciple.fst FStar.Tactics.Util.fst FStar.Reflection.Arith.fst FStar.IO.fst FStar.Map.fst FStar.Monotonic.Witnessed.fst FStar.Classical.fst FStar.Endianness.fst FStar.Tactics.Simplifier.fst FStar.List.Tot.Base.fst FStar.Int.Cast.Full.fst FStar.GSet.fst FStar.Algebra.CommMonoid.Equiv.fst FStar.Integers.fst FStar.Tactics.SyntaxHelpers.fst FStar.LexicographicOrdering.fst FStar.Int.fst FStar.ModifiesGen.fst FStar.Monotonic.Seq.fst FStar.WellFounded.fst FStar.OrdSetProps.fst FStar.Algebra.Monoid.fst FStar.UInt.fst FStar.IFC.fst FStar.Vector.fst FStar.UInt16.fst FStar.Reflection.Formula.fst FStar.Tactics.Arith.fst FStar.Exn.fst FStar.Vector.Properties.fst FStar.HyperStack.fst FStar.List.Pure.fst FStar.Tactics.Effect.fst FStar.Reflection.Derived.Lemmas.fst FStar.Vector.Base.fst FStar.MRef.fst FStar.PCM.fst FStar.Monotonic.HyperHeap.fst FStar.Ghost.fst FStar.Tactics.CanonCommMonoid.fst FStar.Tactics.CanonMonoid.fst FStar.Tactics.Typeclasses.fst FStar.Set.fst FStar.DependentMap.fst FStar.Mul.fst FStar.Preorder.fst FStar.Tactics.PatternMatching.fst FStar.Tactics.CanonCommMonoidSimple.Equiv.fst FStar.List.Pure.Properties.fst FStar.Ref.fst FStar.Int128.fst FStar.Tactics.CanonCommSemiring.fst FStar.Tactics.fst FStar.Tactics.Logic.fst FStar.Tactics.CanonCommSwaps.fst FStar.Fin.fst FStar.Monotonic.Heap.fst FStar.Monotonic.HyperStack.fst FStar.Monotonic.Pure.fst FStar.Tactics.BV.fst FStar.List.fst FStar.Printf.fst FStar.ReflexiveTransitiveClosure.fst FStar.Int8.fst FStar.Order.fst FStar.StrongExcludedMiddle.fst FStar.Seq.Properties.fst FStar.Math.Fermat.fst FStar.UInt128.fst FStar.Tactics.Derived.fst FStar.Monotonic.HyperHeap.fsti FStar.GSet.fsti FStar.LexicographicOrdering.fsti FStar.Int8.fsti FStar.Pervasives.fsti FStar.Int.fsti FStar.ModifiesGen.fsti FStar.Tactics.Types.fsti FStar.UInt64.fsti FStar.Char.fsti FStar.Real.fsti FStar.Set.fsti FStar.Tactics.Effect.fsti FStar.MRef.fsti FStar.Ghost.fsti FStar.Reflection.Data.fsti FStar.UInt.fsti FStar.Universe.fsti FStar.Int64.fsti FStar.BaseTypes.fsti FStar.Reflection.Types.fsti FStar.Tactics.Common.fsti FStar.Int128.fsti FStar.TSet.fsti FStar.Seq.Base.fsti FStar.Modifies.fsti FStar.Monotonic.Witnessed.fsti FStar.IFC.fsti FStar.Float.fsti FStar.BV.fsti FStar.Udp.fsti FStar.Monotonic.Heap.fsti FStar.Vector.Base.fsti FStar.HyperStack.ST.fsti FStar.String.fsti FStar.ReflexiveTransitiveClosure.fsti FStar.Int32.fsti FStar.Monotonic.DependentMap.fsti FStar.Tactics.Builtins.fsti FStar.Tcp.fsti FStar.Math.Euclid.fsti FStar.Squash.fsti FStar.Range.fsti FStar.Reflection.Builtins.fsti FStar.Tactics.Result.fsti FStar.UInt128.fsti FStar.Dyn.fsti FStar.UInt16.fsti FStar.Seq.Properties.fsti FStar.VConfig.fsti FStar.Math.Fermat.fsti FStar.FunctionalExtensionality.fsti FStar.UInt8.fsti FStar.Int16.fsti FStar.BigOps.fsti FStar.DependentMap.fsti FStar.UInt32.fsti FStar.Map.fsti FStar.Date.fsti FStar.Classical.fsti FStar.Monotonic.HyperStack.fsti FStar.Endianness.fsti FStar.Bytes.fsti LowStar.Regional.Instances.fst LowStar.ConstBuffer.fst LowStar.Vector.fst LowStar.BufferOps.fst LowStar.PrefixFreezableBuffer.fst LowStar.Modifies.fst LowStar.Comment.fst LowStar.BufferView.Down.fst LowStar.RVector.fst LowStar.Regional.fst LowStar.BufferView.fst LowStar.Printf.fst LowStar.ImmutableBuffer.fst LowStar.Buffer.fst LowStar.UninitializedBuffer.fst LowStar.Monotonic.Buffer.fst LowStar.ModifiesPat.fst LowStar.Endianness.fst LowStar.BufferView.Up.fst LowStar.BufferView.fsti LowStar.Monotonic.Buffer.fsti LowStar.Literal.fsti LowStar.BufferView.Up.fsti LowStar.Comment.fsti LowStar.Failure.fsti LowStar.ConstBuffer.fsti LowStar.BufferView.Down.fsti LowStar.PrefixFreezableBuffer.fsti legacy/FStar.Error.fst legacy/FStar.Buffer.Quantifiers.fst legacy/FStar.HyperStack.IO.fst legacy/FStar.Pointer.Base.fst legacy/FStar.Buffer.fst legacy/FStar.ErasedLogic.fst legacy/FStar.Pointer.Derived1.fst legacy/FStar.Pointer.fst legacy/FStar.Relational.Relational.fst legacy/FStar.Axiomatic.Array.fst legacy/FStar.Relational.Comp.fst legacy/LowStar.ToFStarBuffer.fst legacy/FStar.Array.fst legacy/FStar.TwoLevelHeap.fst legacy/FStar.Pointer.Derived3.fst legacy/LowStar.BufferCompat.fst legacy/FStar.BufferNG.fst legacy/FStar.Constructive.fst legacy/FStar.Pointer.Derived2.fst legacy/FStar.Crypto.fst legacy/FStar.TaggedUnion.fst legacy/FStar.Matrix2.fsti legacy/FStar.Pointer.Base.fsti legacy/FStar.TaggedUnion.fsti legacy/FStar.Pointer.Derived1.fsti legacy/FStar.Array.fsti legacy/FStar.Pointer.Derived3.fsti legacy/FStar.Pointer.Derived2.fsti experimental/Steel.SelArray.fst experimental/Steel.Channel.Protocol.fst experimental/Steel.FramingTestSuite.fst experimental/FStar.OrdMap.fst experimental/FStar.NMSTTotal.fst experimental/Steel.Effect.Atomic.fst experimental/FStar.InteractiveHelpers.Base.fst experimental/FStar.InteractiveHelpers.PostProcess.fst experimental/Steel.SpinLock.fst experimental/Steel.Primitive.ForkJoin.fst experimental/FStar.InteractiveHelpers.ExploreTerm.fst experimental/Steel.Effect.fst experimental/Steel.Memory.fst experimental/Steel.Reference.fst experimental/FStar.MSTTotal.fst experimental/Steel.Heap.fst experimental/Steel.Utils.fst experimental/FStar.OrdSet.fst experimental/Steel.Effect.M.fst experimental/Steel.MonotonicCounter.fst experimental/Steel.DisposableInvariant.fst experimental/Steel.Preorder.fst experimental/FStar.InteractiveHelpers.fst experimental/Steel.HigherReference.fst experimental/FStar.ConstantTime.Integers.fst experimental/Steel.SelEffect.fst experimental/FStar.MST.fst experimental/FStar.InteractiveHelpers.Output.fst experimental/Steel.Stepper.fst experimental/Steel.Effect.Common.fst experimental/FStar.NMST.fst experimental/Steel.Memory.Tactics.fst experimental/Steel.Primitive.ForkJoin.Unix.fst experimental/Steel.MonotonicHigherReference.fst experimental/Steel.SelEffect.Atomic.fst experimental/FStar.InteractiveHelpers.Effectful.fst experimental/Steel.Semantics.Hoare.MST.fst experimental/FStar.OrdMapProps.fst experimental/FStar.InteractiveHelpers.Propositions.fst experimental/Steel.FractionalPermission.fst experimental/Steel.SelEffect.Common.fst experimental/Steel.Semantics.Instantiate.fst experimental/Steel.Channel.Simplex.fst experimental/Steel.Closure.fst experimental/Steel.DisposableInvariant.fsti experimental/Steel.Channel.Simplex.fsti experimental/Steel.Closure.fsti experimental/Steel.Channel.Duplex.fsti experimental/FStar.OrdMap.fsti experimental/Steel.SelArray.fsti experimental/Steel.Effect.Atomic.fsti experimental/Steel.SelEffect.Atomic.fsti experimental/Steel.HigherReference.fsti experimental/Steel.SpinLock.fsti experimental/Steel.Primitive.ForkJoin.fsti experimental/Steel.Semantics.Instantiate.fsti experimental/Steel.Heap.fsti experimental/FStar.OrdSet.fsti experimental/Steel.LockCoupling.fsti experimental/Steel.Reference.fsti experimental/FStar.ConstantTime.Integers.fsti experimental/Steel.Memory.fsti experimental/Steel.Array.fsti experimental/Steel.SelEffect.Common.fsti experimental/Steel.Effect.Common.fsti experimental/Steel.Effect.fsti experimental/Steel.MonotonicHigherReference.fsti experimental/Steel.SelEffect.fsti > .depend
# [CHECK     prims.fst]
# Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
# (Failure "Empty option")
# make[2]: *** [Makefile.verify:51: .cache/prims.fst.checked] Error 1
# make[2]: Leaving directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# make[1]: *** [Makefile:10: all] Error 2
# make[1]: Leaving directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# make: *** [Makefile:8: all] Error 2

arm32:

#=== ERROR while compiling fstar.2021.06.06 ===================================#
# context              2.1.0 | linux/arm32 | ocaml-base-compiler.4.12.0 | pinned(https://github.com/FStarLang/FStar/archive/refs/tags/v2021.06.06.tar.gz)
# path                 ~/.opam/4.12/.opam-switch/build/fstar.2021.06.06
# command              ~/.opam/opam-init/hooks/sandbox.sh build make PREFIX=/home/opam/.opam/4.12 -j 31
# exit-code            2
# env-file             ~/.opam/log/fstar-12868-39936a.env
# output-file          ~/.opam/log/fstar-12868-39936a.out
### output ###
[...]
# ocamlfind ocamlopt -shared -linkall -thread -package batteries -package zarith -package ppx_deriving.std -package ppx_deriving_yojson -I ulib/tactics_ml ulib/tactics_ml/fstartaclib.cmxa -o ulib/tactics_ml/fstartaclib.cmxs
# [INSTALL   fstartaclib]
# make[3]: Leaving directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# make[2]: Leaving directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# make[1]: Leaving directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib/ml'
# make[1]: Entering directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# make FSTAR_HOME=.. -f Makefile.verify verify-core
# make[2]: Entering directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# ../bin/fstar.exe --warn_error @271   --use_hints --cache_dir .cache --hint_dir .cache --cache_checked_modules --odir _output --dep full  FStar.Pervasives.fst FStar.HyperStack.ST.fst FStar.Seq.Base.fst FStar.Int.Cast.fst FStar.Calc.fst FStar.List.Pure.Base.fst FStar.Reflection.Derived.fst FStar.PredicateExtensionality.fst FStar.Option.fst FStar.Math.Lib.fst FStar.Int32.fst FStar.Tactics.Print.fst FStar.List.Tot.fst FStar.Universe.fst FStar.BV.fst FStar.Math.Euclid.fst FStar.Int64.fst FStar.UInt8.fst FStar.Algebra.CommMonoid.fst FStar.SquashProperties.fst FStar.UInt32.fst FStar.Monotonic.DependentMap.fst FStar.IndefiniteDescription.fst FStar.Monotonic.Map.fst FStar.TSet.fst FStar.Util.fst FStar.UInt64.fst FStar.Heap.fst FStar.All.fst FStar.Squash.fst FStar.Modifies.fst FStar.Tactics.CanonCommMonoidSimple.fst FStar.ST.fst FStar.List.Tot.Properties.fst FStar.Reflection.Const.fst FStar.PropositionalExtensionality.fst FStar.BitVector.fst FStar.HyperStack.All.fst FStar.FunctionalExtensionality.fst FStar.Tactics.Canon.fst FStar.Seq.fst FStar.Seq.Sorted.fst FStar.Reflection.fst FStar.Math.Lemmas.fst FStar.Pervasives.Native.fst FStar.Int16.fst FStar.BigOps.fst FStar.MarkovsPrinciple.fst FStar.Tactics.Util.fst FStar.Reflection.Arith.fst FStar.IO.fst FStar.Map.fst FStar.Monotonic.Witnessed.fst FStar.Classical.fst FStar.Endianness.fst FStar.Tactics.Simplifier.fst FStar.List.Tot.Base.fst FStar.Int.Cast.Full.fst FStar.GSet.fst FStar.Algebra.CommMonoid.Equiv.fst FStar.Integers.fst FStar.Tactics.SyntaxHelpers.fst FStar.LexicographicOrdering.fst FStar.Int.fst FStar.ModifiesGen.fst FStar.Monotonic.Seq.fst FStar.WellFounded.fst FStar.OrdSetProps.fst FStar.Algebra.Monoid.fst FStar.UInt.fst FStar.IFC.fst FStar.Vector.fst FStar.UInt16.fst FStar.Reflection.Formula.fst FStar.Tactics.Arith.fst FStar.Exn.fst FStar.Vector.Properties.fst FStar.HyperStack.fst FStar.List.Pure.fst FStar.Tactics.Effect.fst FStar.Reflection.Derived.Lemmas.fst FStar.Vector.Base.fst FStar.MRef.fst FStar.PCM.fst FStar.Monotonic.HyperHeap.fst FStar.Ghost.fst FStar.Tactics.CanonCommMonoid.fst FStar.Tactics.CanonMonoid.fst FStar.Tactics.Typeclasses.fst FStar.Set.fst FStar.DependentMap.fst FStar.Mul.fst FStar.Preorder.fst FStar.Tactics.PatternMatching.fst FStar.Tactics.CanonCommMonoidSimple.Equiv.fst FStar.List.Pure.Properties.fst FStar.Ref.fst FStar.Int128.fst FStar.Tactics.CanonCommSemiring.fst FStar.Tactics.fst FStar.Tactics.Logic.fst FStar.Tactics.CanonCommSwaps.fst FStar.Fin.fst FStar.Monotonic.Heap.fst FStar.Monotonic.HyperStack.fst FStar.Monotonic.Pure.fst FStar.Tactics.BV.fst FStar.List.fst FStar.Printf.fst FStar.ReflexiveTransitiveClosure.fst FStar.Int8.fst FStar.Order.fst FStar.StrongExcludedMiddle.fst FStar.Seq.Properties.fst FStar.Math.Fermat.fst FStar.UInt128.fst FStar.Tactics.Derived.fst FStar.Monotonic.HyperHeap.fsti FStar.GSet.fsti FStar.LexicographicOrdering.fsti FStar.Int8.fsti FStar.Pervasives.fsti FStar.Int.fsti FStar.ModifiesGen.fsti FStar.Tactics.Types.fsti FStar.UInt64.fsti FStar.Char.fsti FStar.Real.fsti FStar.Set.fsti FStar.Tactics.Effect.fsti FStar.MRef.fsti FStar.Ghost.fsti FStar.Reflection.Data.fsti FStar.UInt.fsti FStar.Universe.fsti FStar.Int64.fsti FStar.BaseTypes.fsti FStar.Reflection.Types.fsti FStar.Tactics.Common.fsti FStar.Int128.fsti FStar.TSet.fsti FStar.Seq.Base.fsti FStar.Modifies.fsti FStar.Monotonic.Witnessed.fsti FStar.IFC.fsti FStar.Float.fsti FStar.BV.fsti FStar.Udp.fsti FStar.Monotonic.Heap.fsti FStar.Vector.Base.fsti FStar.HyperStack.ST.fsti FStar.String.fsti FStar.ReflexiveTransitiveClosure.fsti FStar.Int32.fsti FStar.Monotonic.DependentMap.fsti FStar.Tactics.Builtins.fsti FStar.Tcp.fsti FStar.Math.Euclid.fsti FStar.Squash.fsti FStar.Range.fsti FStar.Reflection.Builtins.fsti FStar.Tactics.Result.fsti FStar.UInt128.fsti FStar.Dyn.fsti FStar.UInt16.fsti FStar.Seq.Properties.fsti FStar.VConfig.fsti FStar.Math.Fermat.fsti FStar.FunctionalExtensionality.fsti FStar.UInt8.fsti FStar.Int16.fsti FStar.BigOps.fsti FStar.DependentMap.fsti FStar.UInt32.fsti FStar.Map.fsti FStar.Date.fsti FStar.Classical.fsti FStar.Monotonic.HyperStack.fsti FStar.Endianness.fsti FStar.Bytes.fsti LowStar.Regional.Instances.fst LowStar.ConstBuffer.fst LowStar.Vector.fst LowStar.BufferOps.fst LowStar.PrefixFreezableBuffer.fst LowStar.Modifies.fst LowStar.Comment.fst LowStar.BufferView.Down.fst LowStar.RVector.fst LowStar.Regional.fst LowStar.BufferView.fst LowStar.Printf.fst LowStar.ImmutableBuffer.fst LowStar.Buffer.fst LowStar.UninitializedBuffer.fst LowStar.Monotonic.Buffer.fst LowStar.ModifiesPat.fst LowStar.Endianness.fst LowStar.BufferView.Up.fst LowStar.BufferView.fsti LowStar.Monotonic.Buffer.fsti LowStar.Literal.fsti LowStar.BufferView.Up.fsti LowStar.Comment.fsti LowStar.Failure.fsti LowStar.ConstBuffer.fsti LowStar.BufferView.Down.fsti LowStar.PrefixFreezableBuffer.fsti legacy/FStar.Error.fst legacy/FStar.Buffer.Quantifiers.fst legacy/FStar.HyperStack.IO.fst legacy/FStar.Pointer.Base.fst legacy/FStar.Buffer.fst legacy/FStar.ErasedLogic.fst legacy/FStar.Pointer.Derived1.fst legacy/FStar.Pointer.fst legacy/FStar.Relational.Relational.fst legacy/FStar.Axiomatic.Array.fst legacy/FStar.Relational.Comp.fst legacy/LowStar.ToFStarBuffer.fst legacy/FStar.Array.fst legacy/FStar.TwoLevelHeap.fst legacy/FStar.Pointer.Derived3.fst legacy/LowStar.BufferCompat.fst legacy/FStar.BufferNG.fst legacy/FStar.Constructive.fst legacy/FStar.Pointer.Derived2.fst legacy/FStar.Crypto.fst legacy/FStar.TaggedUnion.fst legacy/FStar.Matrix2.fsti legacy/FStar.Pointer.Base.fsti legacy/FStar.TaggedUnion.fsti legacy/FStar.Pointer.Derived1.fsti legacy/FStar.Array.fsti legacy/FStar.Pointer.Derived3.fsti legacy/FStar.Pointer.Derived2.fsti experimental/Steel.SelArray.fst experimental/Steel.Channel.Protocol.fst experimental/Steel.FramingTestSuite.fst experimental/FStar.OrdMap.fst experimental/FStar.NMSTTotal.fst experimental/Steel.Effect.Atomic.fst experimental/FStar.InteractiveHelpers.Base.fst experimental/FStar.InteractiveHelpers.PostProcess.fst experimental/Steel.SpinLock.fst experimental/Steel.Primitive.ForkJoin.fst experimental/FStar.InteractiveHelpers.ExploreTerm.fst experimental/Steel.Effect.fst experimental/Steel.Memory.fst experimental/Steel.Reference.fst experimental/FStar.MSTTotal.fst experimental/Steel.Heap.fst experimental/Steel.Utils.fst experimental/FStar.OrdSet.fst experimental/Steel.Effect.M.fst experimental/Steel.MonotonicCounter.fst experimental/Steel.DisposableInvariant.fst experimental/Steel.Preorder.fst experimental/FStar.InteractiveHelpers.fst experimental/Steel.HigherReference.fst experimental/FStar.ConstantTime.Integers.fst experimental/Steel.SelEffect.fst experimental/FStar.MST.fst experimental/FStar.InteractiveHelpers.Output.fst experimental/Steel.Stepper.fst experimental/Steel.Effect.Common.fst experimental/FStar.NMST.fst experimental/Steel.Memory.Tactics.fst experimental/Steel.Primitive.ForkJoin.Unix.fst experimental/Steel.MonotonicHigherReference.fst experimental/Steel.SelEffect.Atomic.fst experimental/FStar.InteractiveHelpers.Effectful.fst experimental/Steel.Semantics.Hoare.MST.fst experimental/FStar.OrdMapProps.fst experimental/FStar.InteractiveHelpers.Propositions.fst experimental/Steel.FractionalPermission.fst experimental/Steel.SelEffect.Common.fst experimental/Steel.Semantics.Instantiate.fst experimental/Steel.Channel.Simplex.fst experimental/Steel.Closure.fst experimental/Steel.DisposableInvariant.fsti experimental/Steel.Channel.Simplex.fsti experimental/Steel.Closure.fsti experimental/Steel.Channel.Duplex.fsti experimental/FStar.OrdMap.fsti experimental/Steel.SelArray.fsti experimental/Steel.Effect.Atomic.fsti experimental/Steel.SelEffect.Atomic.fsti experimental/Steel.HigherReference.fsti experimental/Steel.SpinLock.fsti experimental/Steel.Primitive.ForkJoin.fsti experimental/Steel.Semantics.Instantiate.fsti experimental/Steel.Heap.fsti experimental/FStar.OrdSet.fsti experimental/Steel.LockCoupling.fsti experimental/Steel.Reference.fsti experimental/FStar.ConstantTime.Integers.fsti experimental/Steel.Memory.fsti experimental/Steel.Array.fsti experimental/Steel.SelEffect.Common.fsti experimental/Steel.Effect.Common.fsti experimental/Steel.Effect.fsti experimental/Steel.MonotonicHigherReference.fsti experimental/Steel.SelEffect.fsti > .depend
# [CHECK     prims.fst]
# [CHECK     FStar.Pervasives.Native.fst]
# [CHECK     FStar.Pervasives.fsti]
# FStar.Pervasives.fsti(289,2-289,18): (Error 19) Subtyping check failed; expected type Prims.pure_wp a; got type p: Prims.pure_post a -> Prims.Tot Prims.logical; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(311,38-311,60))
# FStar.Pervasives.fsti(294,2-294,27): (Error 19) Subtyping check failed; expected type Prims.pure_wp b; got type p: Prims.pure_post b -> Prims.Tot Prims.pure_pre; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(311,38-311,60))
# FStar.Pervasives.fsti(299,2-299,40): (Error 19) Subtyping check failed; expected type Prims.pure_wp a; got type post: Prims.pure_post a -> Prims.Tot Prims.logical; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(311,38-311,60))
# FStar.Pervasives.fsti(304,2-304,19): (Error 19) Subtyping check failed; expected type Prims.pure_wp a; got type post: Prims.pure_post a -> Prims.Tot Prims.logical; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(311,38-311,60))
# FStar.Pervasives.fsti(309,2-309,23): (Error 19) Subtyping check failed; expected type Prims.pure_wp a; got type p: Prims.pure_post a -> Prims.Tot Prims.logical; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(311,38-311,60))
# FStar.Pervasives.fsti(314,2-314,17): (Error 19) Subtyping check failed; expected type Prims.pure_wp a; got type p: Prims.pure_post a -> Prims.Tot Prims.logical; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(311,38-311,60))
# FStar.Pervasives.fsti(320,2-320,19): (Error 19) Subtyping check failed; expected type Prims.pure_wp Prims.unit; got type post: Prims.pure_post Prims.unit -> Prims.Tot Prims.logical; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(311,38-311,60))
# FStar.Pervasives.fsti(326,2-326,19): (Error 19) Subtyping check failed; expected type Prims.pure_wp Prims.unit; got type post: Prims.pure_post Prims.unit -> Prims.Tot Prims.logical; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(311,38-311,60))
# FStar.Pervasives.fsti(358,25-358,58): (Error 19) assertion failed; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel (see also prims.fst(311,38-311,60))
# make[2]: *** [Makefile.verify:51: .cache/FStar.Pervasives.fsti.checked] Error 1
# make[2]: Leaving directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# make[1]: *** [Makefile:10: all] Error 2
# make[1]: Leaving directory '/home/opam/.opam/4.12/.opam-switch/build/fstar.2021.06.06/ulib'
# make: *** [Makefile:8: all] Error 2

kit-ty-kate avatar Jul 07 '21 16:07 kit-ty-kate

For the arm32 case, I'd suspect Z3 behaving differently across platforms. For the arm64/ppc64 case, I have no clue.

tahina-pro avatar Jan 20 '22 22:01 tahina-pro

Z3 4.8.5 segfaults on arm64. It returns "Killed" as its only output, but then F* cannot deal with that, raises a fatal exception. Then, F* synthesizes an incorrect backtrace and gives an unrelated error. You need to disable two try/with handlers in the OCaml output, to figure out what's happening.

(At least that's what I had on arm64.)

msprotz avatar Jan 20 '22 23:01 msprotz

If it requires a newer version of Z3, could you have a look at https://github.com/ocaml/opam-repository/pull/20065 I’m not sure if F* expects Z3 to be included statically in the program or not (i suspect it does)

If it wouldn’t be compatible with the way F* expects things to be, could you leave a comment there? (either way it would be appreciated)

kit-ty-kate avatar Jan 20 '22 23:01 kit-ty-kate

I have a different issue on ppc64le, unsure if related.

$ ( checkout, cd to fstar repo etc )
$ git checkout v2022.11.19
$ opam switch show
4.14.0
$ opam install --deps-only .
$ make

Here's the relevant snippet of failing build:

[OCAMLBUILD]
+ ocamlfind ocamlc -c -g -thread -package stdint -package compiler-libs -package compiler-libs.common -package menhirLib -package dynlink -package pprint -package sedlex -package yojson -package ppxlib -package process -package batteries -package zarith -package ppx_deriving.std -package ppx_deriving_yojson -I src/extraction/ml -I ulib/ml -I src/ocaml-output -I src/tests/ml -I src/tactics/ml -I src/prettyprint/ml -I src/parser/ml -I src/fstar/ml -I src/basic/ml -o src/extraction/ml/FStar_Extraction_ML_PrintML.cmo src/extraction/ml/FStar_Extraction_ML_PrintML.ml
File "src/extraction/ml/FStar_Extraction_ML_PrintML.ml", line 196, characters 55-74:
196 |      Ppat_construct (path_to_ident (path', name), Some (build_pattern pat))
                                                             ^^^^^^^^^^^^^^^^^^^
Error: This expression has type
         Ppxlib_ast.Parsetree.pattern = Parsetree.pattern
       but an expression was expected of type
         string Astlib.Ast_414.Asttypes.loc list *
         Ppxlib_ast.Parsetree.pattern
Command exited with code 2.
Compilation unsuccessful after building 255 targets (251 cached) in 00:00:00.

Sadly, I'm not knowledgeable enough about ocaml to know how this might be fixed. At a guess, this is a ppxlib issue, but I don't know what ppxlib is, I just wanted to try out fstar. Luckily I have x86 hardware as well.

The same issue occurs whether or not I opam upgrade z3 from the dependency on 4.8.5 to the current latest version in opam, 4.11.2.

diagprov avatar Jan 19 '23 18:01 diagprov

It's not related, i was able to reproduce on arm64. However I had to use a different set of steps to manage that:

I used opam install --deps-only . before the git checkout v2022.11.19 as master wants ppxlib >= 0.27.0 but v2022.11.19 wants ppxlib >= 0.22.0 & < 0.26.0

So with:

$ ( checkout, cd to fstar repo etc )
$ git checkout v2022.11.19
$ opam switch show
4.14.0
$ opam install --deps-only .
$ make

as you've pasted here works fine for me, but:

$ ( checkout, cd to fstar repo etc )
$ opam install --deps-only .
$ git checkout v2022.11.19
$ opam switch show
4.14.0
$ make

fails with the same error that you've shown. So this should be fixed for you if you do:

$ opam install --deps-only .
$ make

as opam install --deps-only . will downgrade a number of dependencies:

$ opam install --deps .
The following actions will be performed:
=== downgrade 5 packages
  ↘ gen_js_api                  1.1.1 to 1.0.9     [uses ppxlib]
  ↘ ppx_deriving_yojson         3.7.0 to 3.6.1     [required by fstar]
  ↘ ppx_sexp_conv               v0.15.1 to v0.15.0 [uses ppxlib]
  ↘ ppxlib                      0.28.0 to 0.25.1   [required by fstar]
  ↘ sedlex                      3.0 to 2.5         [required by fstar]

kit-ty-kate avatar Jan 19 '23 21:01 kit-ty-kate

Ok, this got me a lot further. Somehow I did indeed have the newer dependencies, so --deps-only downgraded them. I then end up with z3 crashing - I haven't confirmed but I think this is largely the same error you have. Upgrading only z3 (opam upgrade z3) allows checking to almost complete:

experimental/Steel.Preorder.fst(228,4-228,6): (Error 19) could not prove post-condition; The SMT solver could not prove the query. Use --query_stats for more details. (see also experimental/Steel.Preorder.fst(227,78-227,99))
experimental/Steel.Preorder.fst(247,4-247,6): (Error 19) could not prove post-condition; The SMT solver could not prove the query. Use --query_stats for more details. (see also experimental/Steel.Preorder.fst(245,78-245,96)

Of course I'm receiving a lot of warnings like this:

(Warning 282) Expected Z3 version "Z3 version 4.8.5", got "Z3 version 4.11.2 - 64 bit
"
Please download the version of Z3 corresponding to your platform from:
https://github.com/FStarLang/binaries/tree/master/z3-tested
and add the bin/ subdirectory into your PATH

but building z3 myself at 4.8.5 and prepending it to the path so it is used irrespective of ocaml dependencies reproduces your error.

I don't know if these experimental builds can be disabled, I'll have a grep through the source to see if I can find some flags.

diagprov avatar Jan 24 '23 15:01 diagprov