FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Support ppxlib >= 0.26

Open gowthamk opened this issue 2 years ago • 2 comments

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?

gowthamk avatar Aug 17 '22 20:08 gowthamk

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.

tahina-pro avatar Aug 18 '22 00:08 tahina-pro

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.

tahina-pro avatar Aug 18 '22 02:08 tahina-pro

Thanks to @kant2002 for fixing this in #2770.

aseemr avatar Nov 23 '22 07:11 aseemr