sr-lab / coqpyt Goto Github PK

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.

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.

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

Change from main to master

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...

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.

At the moment they are being ignored:
https://github.com/sr-lab/coq-lsp-pyclient/blob/a1e11278e7e48d2a1812ae3d9baeb5b8f4f85432/coqlspclient/coq_file.py#L186

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
• Implement the 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...

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.

Steps to reproduce

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).

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.