Stream: jsCoq

Topic: addon without dune

Hanneli Tavante (May 02 2022 at 23:42):

Hi folks,
Is it possible to pack an addon that currently is not under dune?
Or the easiest way would be to initially "dunify" the lib and then add it to jscoq?
Thanks

Karl Palmskog (May 03 2022 at 06:40):

if it's a regular Coq library, dunifying is generally quick (for example, our template for basic dune file is four lines long). And Dune boilerplate can live alongside other build scripts. Not sure if Dune is required for jsCoq though.

Emilio Jesús Gallego Arias (May 03 2022 at 12:20):

Dune is not a requirement for doing an addon, however it does pay off quickly, in particular when developing jsCoq.

To build an addon without dune, you just need to point the build system of the addon to the right paths of jsCoq's own copy of Coq. Unfortunately we distribute a patched version of Coq, so jsCoq doesn't work against Coq OPAM. I am not sure how easy would be to add these patches to Coq's opam package tho. In this case jscoq could be built against opam's copy.

Emilio Jesús Gallego Arias (May 03 2022 at 12:21):

@Hanneli Tavante look at previous jscoq versions addons directory and you will see a few examples how addons were done before dune

Karl Palmskog (May 03 2022 at 12:22):

@Emilio Jesús Gallego Arias you could do a jsCoq version of the coq package in the core-dev opam repository

Emilio Jesús Gallego Arias (May 03 2022 at 12:22):

But that becomes very annoying quickly if you are going to develop, as you don't get incremental rebuilds, so each time you do make addons everything is done.

Emilio Jesús Gallego Arias (May 03 2022 at 12:22):

Karl Palmskog said:

Emilio Jesús Gallego Arias you could do a jsCoq version of the coq package in the core-dev opam repository

I'm not gonna do that myself, as I don't plan to use it, but I'd be happy to help / support the initiative.

Emilio Jesús Gallego Arias (May 03 2022 at 12:22):

My use case always relies in a composed coq.

Emilio Jesús Gallego Arias (May 03 2022 at 12:23):

That is to say, I'm always hacking both in jsCoq and Coq simultaneously, so I don't use the opam package.

Karl Palmskog (May 03 2022 at 12:23):

sure, then if anyone would be interested in a special opam Coq package for jsCoq, I can add it (if Emilio points at sources/branch to use)

Emilio Jesús Gallego Arias (May 03 2022 at 12:24):

Let's see what Shachar says, but I'm not sure it is worth it, as still opam doesn't provide binary compatiblity. Main use case users have is to build packages that contain .vo , unfortunately with opam, you don't get that. We need something stronger such as docker, so packages built that way can be published in npm.

Emilio Jesús Gallego Arias (May 03 2022 at 12:24):

So I'd wait for someone to have a use case for the jscoq opam package.

Karl Palmskog (May 03 2022 at 12:24):

OK, fine by me

Emilio Jesús Gallego Arias (May 03 2022 at 12:26):

@Hanneli Tavante example of building a non-dunerized addons https://github.com/jscoq/jscoq/blob/v8.12/coq-addons/equations.addon

Hanneli Tavante (May 03 2022 at 14:09):

Thanks folks!
Just wanted to confirm dune indeed would be the most practical way :+1:

Shachar Itzhaky (May 03 2022 at 19:51):

@Emilio Jesús Gallego Arias how about a utility that builds a boilerplate Dune file based on a _CoqProject definition? sounds like it would be helpful for others in porting things.

Hanneli Tavante (May 03 2022 at 20:03):

I'm happy to send a PR improving the docs for the addons + dune if it helps as a short term solution

Shachar Itzhaky (May 03 2022 at 21:11):

that would be wonderful!

Last updated: Jun 01 2023 at 12:01 UTC