Replies: 2 comments 5 replies
-
|
I already fork VSFStar project, but there no substance in it yet, so I do not promote it. I would like to know how do you guys would like to receive external contributions?
Is there anything else which should I do, so you can accept fixes in that area? What's proper location for required test suite? There some |
Beta Was this translation helpful? Give feedback.
-
|
@kant2002, have you seen If you are interested in spending time on it, I would suggest going through Thanks for looking into it! |
Beta Was this translation helpful? Give feedback.
-
|
Yes, I do look at I test on two windows PC. One with Z3 4.8.5 on WSL and second with Z4.8.5 on Cygwin and both produce differences of approximate following kind --- integration.push-pop.out.expected 2022-03-31 14:21:04.000000000 +0600
+++ integration.push-pop.out 2022-04-05 11:17:16.014301400 +0600
@@ -76,7 +76,7 @@
{"kind": "response", "query-id": "75", "response": [], "status": "success"}
{"kind": "response", "query-id": "79", "response": [], "status": "success"}
{"kind": "response", "query-id": "80", "response": [], "status": "success"}
-{"kind": "response", "query-id": "91", "response": [{"level": "error", "message": "Syntax error: Parsing.Parse_error", "number": 168, "ranges": [{"beg": [12, 0], "end": [12, 0], "fname": "<input>"}]}], "status": "success"}
+{"kind": "response", "query-id": "91", "response": [{"level": "error", "message": "Syntax error: Stdlib.Parsing.Parse_error", "number": 168, "ranges": [{"beg": [12, 0], "end": [12, 0], "fname": "<input>"}]}], "status": "success"}
{"kind": "response", "query-id": "98", "response": [], "status": "success"}
{"kind": "response", "query-id": "101", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": "<input>"}, {"beg": [673, 18], "end": [673, 24], "fname": "prims.fst"}]}], "status": "failure"}
{"kind": "response", "query-id": "107", "response": [], "status": "success"}
@@ -92,7 +92,7 @@
{"kind": "response", "query-id": "128", "response": [], "status": "success"}
{"kind": "response", "query-id": "130", "response": [], "status": "success"}
{"kind": "response", "query-id": "133", "response": [], "status": "success"}
-{"kind": "response", "query-id": "137", "response": [{"level": "error", "message": "Syntax error: Parsing.Parse_error", "number": 168, "ranges": [{"beg": [13, 4], "end": [13, 4], "fname": "<input>"}]}], "status": "success"}
+{"kind": "response", "query-id": "137", "response": [{"level": "error", "message": "Syntax error: Stdlib.Parsing.Parse_error", "number": 168, "ranges": [{"beg": [13, 4], "end": [13, 4], "fname": "<input>"}]}], "status": "success"}
{"kind": "response", "query-id": "159", "response": [{"level": "error", "message": "Expected expression of type \"Type0\"; got expression \"Integration.xx\" of type \"nat\"", "number": 189, "ranges": [{"beg": [13, 15], "end": [13, 20], "fname": "<input>"}]}], "status": "success"}
{"kind": "response", "query-id": "163", "response": [], "status": "success"}
{"kind": "response", "query-id": "164", "response": [], "status": "success"}Can you confirm that you see the same? |
Beta Was this translation helpful? Give feedback.
-
|
#2511 is fixing this. |
Beta Was this translation helpful? Give feedback.
-
|
Okay. I take a deep look into https://github.com/FStarLang/FStar/blob/master/tests/interactive/Makefile#L47 I probably create separate folder |
Beta Was this translation helpful? Give feedback.
-
|
Yes, that makes sense. I think the idea is to follow roughly the same style as the tests for the --ide option, but to do something specific for --lsp. |
Beta Was this translation helpful? Give feedback.
-
|
I add tests folder in the #2526 if that changes are fine, then I can work on other issues using that framework. |
Beta Was this translation helpful? Give feedback.
-
Thanks to @kant2002 for opening several recent issues with F*'s --lsp option. #2519 #2523 #2524
So, F*'s support for LSP and its --lsp option was implemented by a contributor as was the corresponding VSCode plugin https://github.com/artagnon/vsfstar, but the latter repo is read-only and the code is no longer maintained.
Clearly, we would all love to have proper support for LSP and more widespread editor integration, and the current code (both in F* and the vsfstar extension) is a useful starting point for such an integration, but as it stands, F*'s --lsp option is not really working properly.
We discussed at today's F* developer's meeting about what to do about this. It would be great to discuss a bit together about how to make progress on this.
Some steps:
Can we get standalone test cases for the --lsp option and include them in the F*'s regression suite? By standalone, I mean tests that can be reproduced from the command line alone, independently of any editor. It might just be a question of collecting some traces by re-enabling tracing. See here artagnon/vsfstar@92627c1 Without such tests, I don't think we can reliably address things like the recently opened issues.
If someone is interested in forking and maintaining the vsfstar plugin, that would be great!
In the long run, reaching parity with the level of functionality offered by fstar-mode.el (F*'s emacs mode) is quite challenging. The main difficulty being the ability to incrementally verify parts of an F* file. However, just supporting vsfstar's existing functionality reliably would already be quite useful.
Beta Was this translation helpful? Give feedback.
All reactions