Skip to content
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

Coq shouldn't require -linkall #9547

Closed
ejgallego opened this issue Feb 11, 2019 · 8 comments
Closed

Coq shouldn't require -linkall #9547

ejgallego opened this issue Feb 11, 2019 · 8 comments
Labels
kind: infrastructure CI, build tools, development tools. part: ocaml resolved: won't fix There are no plans to fix this.
Projects
Dune

Comments

@ejgallego
Copy link
Member

As of today, any executable linking to Coq has to specify -linkall as to properly initialize the parser and some other structures.

IMHO, we should fix our static initialization system so this is not the case.

cc for some discussion: ocaml/dune#1819
@ejgallego ejgallego added the kind: infrastructure CI, build tools, development tools. label Feb 11, 2019
@ejgallego ejgallego added this to Needs review in LSP server Feb 12, 2019
@ejgallego ejgallego moved this from Needs review to To do in LSP server Feb 12, 2019
@ejgallego ejgallego removed this from To do in LSP server Feb 12, 2019
ejgallego added a commit to ejgallego/coq that referenced this issue Feb 13, 2019
@ejgallego
No linkall
2dca115 
Fixes coq#9547
@maximedenes
Copy link
Member

@ejgallego can I assign this issue to you?

@ejgallego
Copy link
Member Author

@ejgallego can I assign this issue to you?

I can't commit to fix this in the short term as it needs some deep coqpp modification; note that I already track issues I've submitted myself anyways.

@Zimmi48
Copy link
Member

Zimmi48 commented Feb 19, 2019

@ejgallego Are these coqpp modifications described somewhere? Would it be appropriate to describe them here or should there be another issue opened about them. If there is such an issue or it is created, then we can label this one as "needs" something (how to put the label name is not yet clear to me though, it doesn't seem to be any of the ones that we already have, or it would have to be generalized).

@ejgallego
Copy link
Member Author

So basically you need coqpp to stop generating static initializers and instead produce a register () function that is called by the users of the grammar files.

Not difficult, but time consuming.

@ejgallego
Copy link
Member Author

No label needed IMHO, what to do is pretty clear [have all the right initializers called in the dep chain]

@Zimmi48
Copy link
Member

Zimmi48 commented Feb 19, 2019

But is this something that you are considering implementing yourself or for which you would prefer to request the help of someone else in @coq/parsing-maintainers? And if so, do they understand the idea?

@ejgallego
Copy link
Member Author

If I have time I'll implement myself but I cannot give a bound now, so anyone is free to take on it of course.

@ejgallego ejgallego added this to Optional / After merge in Dune Feb 21, 2019
@ejgallego ejgallego mentioned this issue May 29, 2019
Closed
ejgallego added a commit to ejgallego/coq that referenced this issue Jan 30, 2020
@ejgallego
[build] Build Coq without linkall
744887d 
This PR is a draft to request for more comments, likely far from final
form yet.

See issue coq#9547

This is also related to PR coq#10951 and coq#7698

We seem to save half to one megabyte in the binaries:

```
-rwxr-xr-x 1 egallego egallego 31651662 janv. 31 00:05 coqc_bin.bc
-rwxr-xr-x 1 egallego egallego 32467231 janv. 31 00:08 coqc_bin.bc

-rwxr-xr-x 1 egallego egallego 23781840 janv. 31 00:05 coqc_bin.exe
-rwxr-xr-x 1 egallego egallego 24395352 janv. 31 00:08 coqc_bin.exe

-rwxr-xr-x 1 egallego egallego 23751520 janv. 31 00:05 coqtop_bin.exe
-rwxr-xr-x 1 egallego egallego 24395608 janv. 31 00:08 coqtop_bin.exe

-rwxr-xr-x 1 egallego egallego 41996191 janv. 31 00:05 coqtop_byte_bin.bc
-rwxr-xr-x 1 egallego egallego 43020328 janv. 31 00:08 coqtop_byte_bin.bc
```
ejgallego added a commit to ejgallego/coq that referenced this issue Jan 30, 2020
@ejgallego
[build] Build Coq without linkall
76c7cf4 
This PR is a draft to request for more comments, likely far from final
form yet.

See issue coq#9547

This is also related to PR coq#10951 and coq#7698

We seem to save half to one megabyte in the binaries:

```
-rwxr-xr-x 1 egallego egallego 31651662 janv. 31 00:05 coqc_bin.bc
-rwxr-xr-x 1 egallego egallego 32467231 janv. 31 00:08 coqc_bin.bc

-rwxr-xr-x 1 egallego egallego 23781840 janv. 31 00:05 coqc_bin.exe
-rwxr-xr-x 1 egallego egallego 24395352 janv. 31 00:08 coqc_bin.exe

-rwxr-xr-x 1 egallego egallego 23751520 janv. 31 00:05 coqtop_bin.exe
-rwxr-xr-x 1 egallego egallego 24395608 janv. 31 00:08 coqtop_bin.exe

-rwxr-xr-x 1 egallego egallego 41996191 janv. 31 00:05 coqtop_byte_bin.bc
-rwxr-xr-x 1 egallego egallego 43020328 janv. 31 00:08 coqtop_byte_bin.bc
```
@ejgallego ejgallego mentioned this issue Jan 30, 2020
Closed
ejgallego added a commit to ejgallego/coq that referenced this issue Jan 30, 2020
@ejgallego
[build] Build Coq without linkall
e84adf4 
This PR is a draft to request for more comments, likely far from final
form yet.

See issue coq#9547

This is also related to PR coq#10951 and coq#7698

We seem to save half to one megabyte in the binaries:

```
-rwxr-xr-x 1 egallego egallego 31651662 janv. 31 00:05 coqc_bin.bc
-rwxr-xr-x 1 egallego egallego 32467231 janv. 31 00:08 coqc_bin.bc

-rwxr-xr-x 1 egallego egallego 23781840 janv. 31 00:05 coqc_bin.exe
-rwxr-xr-x 1 egallego egallego 24395352 janv. 31 00:08 coqc_bin.exe

-rwxr-xr-x 1 egallego egallego 23751520 janv. 31 00:05 coqtop_bin.exe
-rwxr-xr-x 1 egallego egallego 24395608 janv. 31 00:08 coqtop_bin.exe

-rwxr-xr-x 1 egallego egallego 41996191 janv. 31 00:05 coqtop_byte_bin.bc
-rwxr-xr-x 1 egallego egallego 43020328 janv. 31 00:08 coqtop_byte_bin.bc
```
ejgallego added a commit to ejgallego/coq that referenced this issue Mar 27, 2021
@ejgallego
[plugins] Support for a findlib-based loader.
61be049 
We introduce new syntax
```
Require ML Module pkg1 ... pkgn.
```
that uses findlib to locate and load a Coq plugin and its dependencies.

This makes feasible to actually develop Coq plugins that depend on
OCaml libraries not linked into the Coq main binaries without hitting
problems.

Fixes coq#5028, fixes coq#7698 .

This provides a workaround for coq#12607 , and helps with coq#9547 .
@ejgallego ejgallego mentioned this issue Mar 27, 2021
Closed
ejgallego added a commit to ejgallego/coq that referenced this issue Sep 10, 2021
@ejgallego
[plugins] Support for a findlib-based loader.
1609a75 
We introduce new syntax
```
Require ML Module pkg1 ... pkgn.
```
that uses findlib to locate and load a Coq plugin and its dependencies.

This makes feasible to actually develop Coq plugins that depend on
OCaml libraries not linked into the Coq main binaries without hitting
problems.

Fixes coq#5028, fixes coq#7698 .

This provides a workaround for coq#12607 , and helps with coq#9547 .
@ejgallego
Copy link
Member Author

Note that #15220 and in general proper plugin linking in OCaml seems to require -linkall.

This is very unfortunate, but we don't have a short term fix for now :S

Dune automation moved this from Forward to Dune to Done Jan 27, 2022
@ejgallego ejgallego added part: ocaml resolved: won't fix There are no plans to fix this. labels Jan 27, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: infrastructure CI, build tools, development tools. part: ocaml resolved: won't fix There are no plans to fix this.
Projects
Dune
  
Done
Milestone
No milestone
Development

No branches or pull requests
3 participants
@maximedenes @Zimmi48 @ejgallego