Segmentation Fault when loading 'coq/theories/Numbers/Cyclic/Int63/PrimInt63.v'

[laetitia-teo]

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

[Nfsaavedra]

Hello @laetitia-teo,

I did some debugging and the segmentation fault apparently comes from coq-lsp, so we can't do much about it. Your best option is probably to create an issue in coq-lsp to see if they can fix the bug.

You can also try to use the last version of coq-lsp in the main branch and check if it fixes the problem.

[ejgallego]

Hi folks, thanks for your patience, this is a

Duplicate of rocq-archive/coq-serapi#397

I've fixed the bug, an updated coq-serapi version should appear soon in Opam.

[Nfsaavedra]

Hi folks, thanks for your patience, this is a

Duplicate of ejgallego/coq-serapi#397

I've fixed the bug, an updated coq-serapi version should appear soon in Opam.

Thanks @ejgallego!

[ejgallego]

Hi folks, fixed versions are being released into opam (cc: ocaml/opam-repository#25552 for 8.19, etc... )

You can close this issue IMHO