Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Syntax accepted in emacs language server but not on the command line for a depends run #3536

Open
briangmilnes opened this issue Oct 7, 2024 · 0 comments

Comments

@briangmilnes
Copy link
Contributor

module ParseBug

open FStar.String

let aneq s1 s2 (pos: nat{pos <= strlen s1 && pos <= strlen s2}) =
strlen s1 = strlen s2 /
forall (i: nat{i < pos}). index s1 i = index s2 i

// This parses in emacs bug not on the command line fstar.exe depend call.
// qmake libs
// Forge: DEPEND _build
// F
orge: DEPEND _build/fstar
// [ -d _build/fstar ] || mkdir -p _build/fstar;
// Forge: DEPEND _build/fstar/ml
// [ -d _build/fstar/fst/checked ] || mkdir -p _build/fstar/fst/checked
// F
orge: DEPEND _build/fstar/depend
// /home/milnes/.opam/default/bin/fstar.exe --warn_error "-321-333-331-274-241-247" --use_hints --use_hint_hashes --record_hints --hint_dir _build/fstar/fst/hints --print_universes // --print_implicits --cache_checked_modules --dep full --output_deps_to _build/fstar/depend --cache_dir _build/fstar/fst/checked --include src src/ParseBug.fst
// * Error 168 at src/ParseBug.fst(7,8-7,8):
// - Syntax error
// /Tuff/exps/parsebug $ fstar.exe --version
// F* 2024.08.14
dev
// platform=Linux_x86_64
// compiler=OCaml 4.14.2
// date=2024-09-02 15:23:16 -0700
// commit=445f713ad8b276864ba7e205e028813e19324b66

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant