rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
45 stars 25 forks source link

[CN] Repackage CN as separate library and executable #315

Closed samcowger closed 1 month ago

samcowger commented 2 months ago

Currently, CN is packaged as an executable (in dune terms). As far as I can tell, this makes it impossible for other OCaml packages/projects to import/rely on CN modules, because (again, as far as I can tell - my OCaml/opam/dune is rusty) projects can only depend on libraries, not executables. Assuming the choice of this shape of packaging was arbitrary, I think we ought to reorganize things such that other projects can depend on CN, and can import the bulk of CN's modules.

One approach could look something like:

Some local experimentation suggests this approach is viable. Though a directory shuffle ought to have negligible impact on CN development in general, I realize it would be a bit painful immediately, especially for anyone with unmerged CN changes lying around. How does this land with folks? Does it seem like a good idea, and/or does it seem burdensome?

dc-mak commented 2 months ago

Related: https://github.com/rems-project/cerberus/issues/308

samcowger commented 2 months ago

Related: #308

Aha - I went looking for related issues but didn't see this one, thanks for the pointer! It seems like that issue is more about repo-splitting, and that the library/executable splitting I'm proposing here would work in tandem with (at best help, at worst not harm) that effort. Does that seem right?

dc-mak commented 2 months ago

Correct; though I think it is unwise to parallelise major refactors and we might be able to move a little faster on this after the repo splitting.

thatplguy commented 2 months ago

@samcowger is building an OCaml implementation of the language server with the intention of linking against CN as a library, rather than invoking it from the command line.

@samcowger, are you blocked on this refactoring? If so, it would make sense to do this first, unless @dc-mak has already started the repo split on a branch.

samcowger commented 2 months ago

I've successfully implemented the lib/exe split locally, so I can probably make progress and quasi-maintain it while the repo-splitting is in progress, though if I need to rebase on changes to CN, it could be a bit finicky.

Has work on that split begun?

dc-mak commented 2 months ago

@kmemarian will be able to comment precisely - it’s substantially underway I believe.

I think library splitting first is also fine, but I guess I’m just slightly wary of both at the same time and then someone needing to rebase/redo all the work again so please hold fire (annoying I know, but better safe than sorry, and better smooth than rough).

samcowger commented 2 months ago

it’s substantially underway I believe.

In that case, no worries! I don't want to step on any toes. We can revisit this once that's done, unless this accidentally gets taken care of in the process.

samcowger commented 1 month ago

Just checking in - @kmemarian, how is the repo split progressing?

dc-mak commented 1 month ago

We've been sidelined with POPL deadline, which has now passed. We'll all be taking a few days to recover, and we can give an update then.

dc-mak commented 1 month ago

Hi @samcowger , we discussed and we think the repo split/refactor will take some time yet and the changes to backend/cn should be small, so we should proceed with this now. Sorry for the double delay (in getting back, and in holding this up), and thank you for the suggestion and work.

samcowger commented 1 month ago

Alrighty, thanks! I'll put together a PR, and we can figure out how best to merge it without too much disruption.