FStar
FStar copied to clipboard
Support ppxlib >= 0.26
With ppxlib.0.27.0
, fstar.2022.08.10~dev
compilation fails with the following error:
#=== ERROR while compiling fstar.2022.08.10~dev ===============================#
# context 2.1.0 | macos/x86_64 | ocaml-base-compiler.4.12.0 | pinned(git+ssh://[email protected]/FStarLang/FStar.git#c625bb4f)
# path ~/.opam/4.12.0/.opam-switch/build/fstar.2022.08.10~dev
# command ~/.opam/opam-init/hooks/sandbox.sh build make PREFIX=/Users/gkaki/.opam/4.12.0 -j 7
# exit-code 2
# env-file ~/.opam/log/fstar-40230-052316.env
# output-file ~/.opam/log/fstar-40230-052316.out
### output ###
# [...]
# + ocamlfind ocamlc -c -g -thread -package stdint -package compiler-libs -package compiler-libs.common -package menhirLib -package dynlink -package pprint -p
ackage sedlex -package yojson -package ppxlib -package process -package batteries -package zarith -package ppx_deriving.std -package ppx_deriving_yojson -I sr
c/extraction/ml -I src/ocaml-output -I src/parser/ml -I src/basic/ml -I src/tests[...]
# File "src/extraction/ml/FStar_Extraction_ML_PrintML.ml", line 195, characters 55-74:
# 195 | Ppat_construct (path_to_ident (path', name), Some (build_pattern pat))
# ^^^^^^^^^^^^^^^^^^^
# Error: This expression has type
# Ppxlib_ast.Parsetree.pattern = Astlib.Ast_414.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.
# make[1]: *** [_build/src/fstar/ml/main.native] Error 10
# make: *** [all] Error 2
ppxlib's changelog describes non-trivial changes to the ppxlib AST pushed in version 0.26.0. Maybe the dependency on ppxlib in fstar.opam needs to have an upper bound?
Thank you for reporting. f6dc2f1bf910d6f206c489197296c2700db442d2 is doing exactly that, and I'll be merging it soon if CI allows it.
However, ideally, we should rather fix FStar_Extraction_ML_PrintML.ml
if possible. So, I consider this commit as a stopgap solution for now.
Just merged. (As an aside, someone also set such an upper bound for the latest published opam package: ocaml/opam-repository#21990
Let me now repurpose this issue to ask for help fixing FStar_Extraction_ML_PrintML.ml
to support ppxlib >= 0.26.
Thanks to @kant2002 for fixing this in #2770.