verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
73 stars 20 forks source link

Unify our three separate dune builds #400

Closed hackedy closed 1 year ago

hackedy commented 1 year ago

Currently there are three distinct dune-project roots corresponding to three separate OPAM packages.

The build system builds the stuff in deps first, then installs it to the global OPAM folders on your machine, and then builds petr4 treating the dependencies as external packages. This is bad--it clobbers any installed version of poulet4 you might have. It also makes incremental builds break in weird ways and prevents parallelism.

The changes in this PR reorganize the repo so that everything is associated with a single dune-project but it retains the separate opam packages, which aren't installed until you actually ask dune or OPAM to install them. All build files go in _build in the root instead of being scattered across separate _build dirs.

I know the diff looks huge but most of it is directory changes along these lines:

./deps/poulet4        -->  ./coq
./deps/poulet4_Ccomp  -->  ./ccomp

There were noticeable improvements to build time for a clean build. But I expect the main quality of life improvement will be in incremental builds.

BUILD RESULTS
old style: 274.11s user 123.15s system 275% cpu 2:24.42 total
new style: 319.90s user 123.01s system 466% cpu 1:35.00 total
QinshiWang commented 1 year ago

This will not support only building and installing poulet4 but not poulet4_Ccomp in order to test VerifiableP4, right?

hackedy commented 1 year ago

This will not support only building and installing poulet4 but not poulet4_Ccomp in order to test VerifiableP4, right?

I just took a look and

dune build -p poulet4
dune install poulet4

only builds and installs poulet4 👍