sr-lab / coqpyt Goto Github PK
View Code? Open in Web Editor NEWPython client for coq-lsp
License: MIT License
Python client for coq-lsp
License: MIT License
At the moment ProofState is very slow for use cases such as simulating an interaction with a Coq file. Maybe we need a cache for the libraries being loaded. If we implement #13, this issue is possibly fixed as well but we will need to check.
The current implementation is buggy. @pcarrott please add more details to this issue
The AST returned by Coq includes a final step with whatever white space and comments are found after the last step in the file. This step is currently being treated as a regular step. However, it is not possible to add steps after it because its range needs to be handled differently. We are not aware of other unexpected behaviours.
Changes should be made to how this step is handled, whether the last step should be ignored (it holds no relevant information) or if we should treat the last step differently where appropriate.
Hi,
I've been plagued with segfaults when opening a particular file from the standard library ('coq/theories/Numbers/Cyclic/Int63/PrimInt63.v').
I'm on Ubuntu 20.04.3 LTS.
Pretty straightforward, the error happens on file open.
# Open Coq file
with CoqFile('/home/<user>/.opam/default/lib/coq/theories/Numbers/Cyclic/Int63/PrimInt63.v') as coq_file:
pass
Looking into more detail, the segfault happens on flushing of the BufferedWriter in the json rpc endpoint, when sending a 'coq\getDocument'
request (/coqpyt/coqpyt/lsp/json_rpc_endpoint.py
, line 61):
def send_request(self, message): # message['method'] == 'coq/getDocument'
"""
Sends the given message.
:param dict message: The message to send.
"""
try:
json_string = json.dumps(message, cls=MyEncoder)
jsonrpc_req = self.__add_header(
with self.write_lock:
self.stdin.write(jsonrpc_req.encode())
self.stdin.flush() # happens here
except BrokenPipeError as e:
logging.error(e)
I've tried reinstalling coq, using different versions of python, to no avail. Any idea of what might be happening here? This also only show up for this particular file (other coq standard theories are fine).
Using the latest code on master, I tried running pytest test -s
as instructed but had 3 failed tests and 2 tests with errors. Are these errors expected?
Here is the test summary:
FAILED tests/test_coq_file.py::test_derive[test_derive.v] - TypeError: sequence item 0: expected str instance, NoneType found FAILED tests/test_readme.py::test_readme_example - AssertionError: assert 1 == 0 FAILED tests/proof_file/test_changes.py::TestProofChangeNestedProofs::test_change_nested_proofs - coqpyt.coq.exceptions.InvalidFileException: The file /tmp/teste79ae2f8a3334fce8831de9fcf0a6cd5.v is not valid. FAILED tests/proof_file/test_proof_file.py::TestProofNestedProofs::test_nested_proofs - AssertionError: assert 3 == 5 ERROR tests/proof_file/test_changes.py::TestProofChangeObligation::test_change_obligation - RuntimeError: Unknown obligation command with tag number 1: Obligation 2 of id2. ERROR tests/proof_file/test_proof_file.py::TestProofObligation::test_obligation - RuntimeError: Unknown obligation command with tag number 1: Obligation 2 of id2.
I'm trying to run the tests on my macmini, but each time the program prints a lot of
"
/bin/sh: line 0: ulimit: virtual memory: cannot modify limit: Invalid argument
/bin/sh: line 0: ulimit: virtual memory: cannot modify limit: Invalid argument
..."
after looking up the code, I changed the 60 line of coqlspclient/coq_lsp_client.py, turning the "ulimit -v {memory_limit};" into "ulimit -v unlimited;" then the annoying messages disappeared.
I'm not sure whether it's the fault of the ulimit command or macos...
As the Coq version changes, the AST provided by Coq also changes. We should support the same versions supported by coq-lsp. To do so, a parameter to define what is the Coq version to be used in the class CoqFile
should be implemented. As the parameter changes, we should handle the AST accordingly.
The index parameter in add_step
is the index of the step succeeding the new step. This does not allow steps to be added to the beginning of the file (i.e., when there is no previous step). The index parameter should be changed to reflect the index of the new step.
Class Reflexive (R : A -> A -> Prop) := reflexivity : forall x : A, R x x.
The statement above from the Coq standard library generates a theorem called reflexivity
. This theorem can be used with apply reflexivity
, but the tactic reflexivity
can still be used as well. This is a problem since when we are collecting our context the statement above will be linked to the tactic reflexivity
, even when it shouldn't.
Our context should allow equal names with different term types and then somehow figure out what is the correct term type to be collected in different situations.
Change from main to master
Support adding and removing steps from a Coq file from Python. coq-lsp-pyclient
should be able to go back and forward in the execution of the file.
General steps to implement (by @pcarrott):
ProofState
is changed to be a child class of CoqFile
called ProofFile
CoqFile
is changed to support writing in a similar way to AuxFile
sign
in the exec
of CoqFile
. For now, we will only support this inside proofs to avoid having to remove terms that were already defined, having to change the module while going backwards, etc...At the moment they are being ignored:
https://github.com/sr-lab/coq-lsp-pyclient/blob/a1e11278e7e48d2a1812ae3d9baeb5b8f4f85432/coqlspclient/coq_file.py#L186
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.