tahina-pro
commented
2 years ago For the arm32 case, I'd suspect Z3 behaving differently across platforms. For the arm64/ppc64 case, I have no clue.
Open kit-ty-kate opened 3 years ago
tahina-pro
commented
2 years ago For the arm32 case, I'd suspect Z3 behaving differently across platforms. For the arm64/ppc64 case, I have no clue.
msprotz
commented
2 years ago 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.)
kit-ty-kate
commented
2 years ago 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)
diagprov
commented
1 year ago 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 .
$ makeHere'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.
kit-ty-kate
commented
1 year ago 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 .
$ makeas 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
$ makefails with the same error that you've shown. So this should be fixed for you if you do:
$ opam install --deps-only .
$ makeas 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]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 PATHbut 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.
arm64 and ppc64:
arm32: