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

LSP server failed to load deps #2523

Open
kant2002 opened this issue Apr 2, 2022 · 3 comments
Open

LSP server failed to load deps #2523

kant2002 opened this issue Apr 2, 2022 · 3 comments

Comments

@kant2002
Copy link
Contributor

kant2002 commented Apr 2, 2022

Windows. Install FStar.exe from https://github.com/FStarLang/FStar/releases/tag/v2022.03.24 and from https://github.com/FStarLang/FStar/releases/tag/v2022.01.15

When using https://marketplace.visualstudio.com/items?itemName=artagnon.vsfstar which simply run fstar.exe --lsp I see following error in the Output of VS Code.

[E] Failed to load deps

Same VSCode plugin on Linux has no issues. How can I further troubleshoot issue?

@kant2002
Copy link
Contributor Author

kant2002 commented Apr 3, 2022

After applying #2528

For example I open src/fstar/FStar.CheckedFiles.fst. then in the F* Language Server output I receive following message

[E] Failed to load deps. Recursive dependency on module ~/FStar/src/basic/FStar.Options.fst

When open FStar.Parser.Dep.fst I receive following error

[E] Failed to load deps. Error You may have a cyclic dependence on module fstar.parser.dep: use --dep full to confirm. Alternatively, invoking fstar with /home/kant/FStar/src/parser/FStar.Parser.Dep.fst on the command line breaks the abstraction imposed by its interface /home/kant/FStar/src/parser/FStar.Parser.Dep.fsti; if you really want this behavior add the option '--expose_interfaces'

@kant2002
Copy link
Contributor Author

Here the output for troubleshooting when open file src/basic/FStar.Const.fst

The cycle contains a subset of the modules in:
/home/kant/FStar/ulib/FStar.Set.fst                                                  <=====
`used by` /home/kant/FStar/ulib/FStar.Util.fst
`used by` /home/kant/FStar/src/basic/FStar.Options.fst
`used by` /home/kant/FStar/src/parser/FStar.Parser.Const.fst
`used by` /home/kant/FStar/src/reflection/FStar.Reflection.Data.fst
`used by` /home/kant/FStar/ulib/FStar.Tactics.Builtins.fsti
`used by` /home/kant/FStar/ulib/FStar.FunctionalExtensionality.fst
`used by` /home/kant/FStar/ulib/FStar.Set.fst                                        <=====
`used by` /home/kant/FStar/ulib/FStar.ST.fst
`used by` /home/kant/FStar/ulib/FStar.All.fst
`used by` /home/kant/FStar/ulib/FStar.String.fsti
`used by` /home/kant/FStar/src/basic/FStar.Compiler.Range.fst
`used by` /home/kant/FStar/src/basic/FStar.Ident.fsti 
A DOT-format graph has been dumped in the current directory as dep.graph
With GraphViz installed, try: fdp -Tpng -odep.png dep.graph
Hint: cat dep.graph | grep -v _ | grep -v prims

[E] Failed to load deps. Error Recursive dependency on module /home/kant/FStar/ulib/FStar.Set.fst
Content-Length: 146

{"jsonrpc":"2.0","method":"textDocument/publishDiagnostics","params":{"uri":"file:///home/kant/FStar/src/basic/FStar.Const.fst","diagnostics":[]}}Content-Length: 38

I use custom #2528 with changed Makefile

FSTAR:=${FSTAR_HOME}/bin/fstar.exe $(SMT) --lsp --warn_error -282 \
	--include ${FSTAR_HOME} \
	--include ${FSTAR_HOME}/src/basic \
	--include ${FSTAR_HOME}/src/extraction \
	--include ${FSTAR_HOME}/src/fstar \
	--include ${FSTAR_HOME}/src/parser \
	--include ${FSTAR_HOME}/src/reflection \
	--include ${FSTAR_HOME}/ulib

@kant2002
Copy link
Contributor Author

For information, the VSCode extension pass root directory and all subdirectories to --lsp mode.

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