Consider merging "examples" into this repository
We now have the setup to be able to merge iris/examples into this repository. But do we want to?
Advantages:
- When prototyping changes in Iris we very quickly get some feedback on the impact on reverse dependencies.
- It's one repository less that Robbert and me have to port changes to.
- People trying to fix Coq CI have one repository less to worry about.
Downsides:
-
make
will require Autosubst to fully work -
make
in Iris will take quite a bit longer - CI will take longer before a package is published in opam
I don't have a very strong opinion on this. Very rarely I make changes that break something in iris/examples in subtle ways and debugging that would be much easier in a mono repo. But most of the time the overhead from having two repositories is not so bad, and it's nice that people don't have to install Autosubst to make make
work.