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.

Sign up for GitHub

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

Jump to bottom

Segmentation fault in coq/getDocument call #397

Closed

Nfsaavedra opened this issue Mar 6, 2024 · 4 comments · Fixed by #398, ocaml/opam-repository#25552, ocaml/opam-repository#25570 or ocaml/opam-repository#25571

Labels

kind: bug kind: serialization kind: upstream

Milestone

Nfsaavedra commented Mar 6, 2024 •

edited

Loading

Describe the bug
coq-lsp raises a segmentation fault when coq/getDocument is called on the file Coq.Numbers.Cyclic.Int63.PrimInt63 or Coq.Floats.PrimFloat of the Coq standard library.

To Reproduce
Steps to reproduce the behavior:

Do a coq/getDocument call on the Coq.Numbers.Cyclic.Int63.PrimInt63 or Coq.Floats.PrimFloat file.

Expected behavior
Return the document instead of raising a segmentation fault.

Desktop

Pop!_OS 22.04 LTS/Ubuntu 20.04.3 LTS/Ubuntu 22.04.2 LTS
coq-lsp 0.1.8 (I think the issue also happens in 0.1.7)

Additional context
This issue is related to sr-lab/coqpyt#35.

The text was updated successfully, but these errors were encountered:

Nfsaavedra added the kind: bug label

Nfsaavedra changed the title ~~Segmentation fault in coq\getDocument call~~ Segmentation fault in coq/getDocument call

Collaborator

Alizter commented Mar 6, 2024

@Nfsaavedra What version of Coq is this for?

Author

Nfsaavedra commented Mar 6, 2024

@Nfsaavedra What version of Coq is this for?

8.18 when using 0.1.8. 8.17 when using 0.1.7.

Collaborator

ejgallego commented Mar 6, 2024

That's for sure a SerAPI bug, thanks a lot for the report.

Collaborator

ejgallego commented Mar 6, 2024 •

edited

Loading

SerAPI has to do some unsafe code to serialize all the Coq Ast, very unfortunately. coq-lsp has no unsafe code and should not segfault.

I will have a look, but it is possible that this is fixed on main.

ejgallego transferred this issue from ejgallego/coq-lsp

ejgallego added this to the 0.17.3 milestone

ejgallego added kind: serialization kind: upstream labels

ejgallego added a commit that referenced this issue


          [serlib] Fix TODO / bug in primitive code.

2dbc5ab

That was a quite dumb TODO I forgot about. But indeed, GADT remain an
issue for us.

Fixes #397 , fixes sr-lab/coqpyt#35

Thanks to Laetitia Teodorescu (@laetitia-teo) and Nuno
Saavedra (@Nfsaavedra) for the bug report.

ejgallego mentioned this issue

Segmentation Fault when loading 'coq/theories/Numbers/Cyclic/Int63/PrimInt63.v' sr-lab/coqpyt#35

Closed

ejgallego added a commit that referenced this issue


          [serlib] Fix TODO / bug in primitive code.

74d5696

That was a quite dumb TODO I forgot about. But indeed, GADT remain an
issue for us.

Fixes #397 , fixes sr-lab/coqpyt#35

Thanks to Laetitia Teodorescu (@laetitia-teo) and Nuno
Saavedra (@Nfsaavedra) for the bug report.

ejgallego mentioned this issue

[serlib] Fix TODO / bug in primitive code. #398

Merged

ejgallego added a commit that referenced this issue


          [serlib] Fix TODO / bug in primitive code.

4219b5e

That was a quite dumb TODO I forgot about. But indeed, GADT remain an
issue for us.

Fixes #397 , fixes sr-lab/coqpyt#35

Thanks to Laetitia Teodorescu (@laetitia-teo) and Nuno
Saavedra (@Nfsaavedra) for the bug report.

ejgallego added a commit that referenced this issue


          [serlib] Fix TODO / bug in primitive code.

da6ba69

That was a quite dumb TODO I forgot about. But indeed, GADT remain an
issue for us.

Fixes #397 , fixes sr-lab/coqpyt#35

Thanks to Laetitia Teodorescu (@laetitia-teo) and Nuno
Saavedra (@Nfsaavedra) for the bug report.

ejgallego added a commit that referenced this issue


          [serlib] Fix TODO / bug in primitive code.

85d2bc1

That was a quite dumb TODO I forgot about. But indeed, GADT remain an
issue for us.

Fixes #397 , fixes sr-lab/coqpyt#35

Thanks to Laetitia Teodorescu (@laetitia-teo) and Nuno
Saavedra (@Nfsaavedra) for the bug report.

ejgallego closed this as completed in #398

ejgallego added a commit that referenced this issue


          [serlib] Fix TODO / bug in primitive code.

a3ea9ff

That was a quite dumb TODO I forgot about. But indeed, GADT remain an
issue for us.

Fixes #397 , fixes sr-lab/coqpyt#35

Thanks to Laetitia Teodorescu (@laetitia-teo) and Nuno
Saavedra (@Nfsaavedra) for the bug report.

ejgallego mentioned this issue

[new release] coq-serapi (8.19.0+0.19.2) ocaml/opam-repository#25552

Merged

ejgallego added a commit to ejgallego/opam-repository that referenced this issue


          [new release] coq-serapi (8.19.0+0.19.2)

667ba24

CHANGES:

 - [serlib] Fix (@ejgallego, rocq-archive/coq-serapi#398, fixes rocq-archive/coq-serapi#397 fixes sr-lab/coqpyt#35 ,
            thanks to @laetitia-teo and @Nfsaavedra for the bug
            report)

ejgallego added a commit that referenced this issue


          [serlib] Fix TODO / bug in primitive code.

bc3450a

That was a quite dumb TODO I forgot about. But indeed, GADT remain an
issue for us.

Fixes #397 , fixes sr-lab/coqpyt#35

Thanks to Laetitia Teodorescu (@laetitia-teo) and Nuno
Saavedra (@Nfsaavedra) for the bug report.

ejgallego added a commit to ejgallego/opam-repository that referenced this issue


          [new release] coq-serapi (8.18.0+0.18.3)

2ee8b4c

CHANGES:

 - [serlib] Fix (@ejgallego, rocq-archive/coq-serapi#398, fixes rocq-archive/coq-serapi#397 fixes sr-lab/coqpyt#35 ,
            thanks to @laetitia-teo and @Nfsaavedra for the bug
            report)

ejgallego added a commit to ejgallego/opam-repository that referenced this issue


          [new release] coq-serapi (8.18.0+0.18.3)

fc53912

CHANGES:

 - [serlib] Fix (@ejgallego, rocq-archive/coq-serapi#398, fixes rocq-archive/coq-serapi#397 fixes sr-lab/coqpyt#35 ,
            thanks to @laetitia-teo and @Nfsaavedra for the bug
            report)

ejgallego mentioned this issue

[new release] coq-serapi (8.18.0+0.18.3) ocaml/opam-repository#25570

Merged

ejgallego added a commit that referenced this issue


          [serlib] Fix TODO / bug in primitive code.

ba1550a

That was a quite dumb TODO I forgot about. But indeed, GADT remain an
issue for us.

Fixes #397 , fixes sr-lab/coqpyt#35

Thanks to Laetitia Teodorescu (@laetitia-teo) and Nuno
Saavedra (@Nfsaavedra) for the bug report.

ejgallego added a commit that referenced this issue


          [serlib] Fix TODO / bug in primitive code.

9c3f5bf

That was a quite dumb TODO I forgot about. But indeed, GADT remain an
issue for us.

Fixes #397 , fixes sr-lab/coqpyt#35

Thanks to Laetitia Teodorescu (@laetitia-teo) and Nuno
Saavedra (@Nfsaavedra) for the bug report.

ejgallego added a commit to ejgallego/opam-repository that referenced this issue


          [new release] coq-serapi (8.17.0+0.17.3)

7dd562b

CHANGES:

 - [serlib] Fix (@ejgallego, rocq-archive/coq-serapi#398, fixes rocq-archive/coq-serapi#397 fixes sr-lab/coqpyt#35 ,
            thanks to @laetitia-teo and @Nfsaavedra for the bug
            report)

ejgallego mentioned this issue

[new release] coq-serapi (8.17.0+0.17.3) ocaml/opam-repository#25571

Merged

ejgallego added a commit to ejgallego/opam-repository that referenced this issue


          [new release] coq-serapi (8.17.0+0.17.3)

61982cd

CHANGES:

 - [serlib] Fix (@ejgallego, rocq-archive/coq-serapi#398, fixes rocq-archive/coq-serapi#397 fixes sr-lab/coqpyt#35 ,
            thanks to @laetitia-teo and @Nfsaavedra for the bug
            report)

ejgallego added a commit to ejgallego/opam-repository that referenced this issue


          [new release] coq-serapi (8.18.0+0.18.3)

d3ca2e3

CHANGES:

 - [serlib] Fix (@ejgallego, rocq-archive/coq-serapi#398, fixes rocq-archive/coq-serapi#397 fixes sr-lab/coqpyt#35 ,
            thanks to @laetitia-teo and @Nfsaavedra for the bug
            report)

ejgallego added a commit to ejgallego/opam-repository that referenced this issue


          [new release] coq-serapi (8.19.0+0.19.2)

0f14a8c

CHANGES:

 - [serlib] Fix (@ejgallego, rocq-archive/coq-serapi#398, fixes rocq-archive/coq-serapi#397 fixes sr-lab/coqpyt#35 ,
            thanks to @laetitia-teo and @Nfsaavedra for the bug
            report)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment