Use dune for installing the files in share

[psafont]

This allows to drop ad-hoc shell scripts that were used for installing the 'libdirs' of the tools.
Dune is able to do install entire source trees starting from version 3.11. The only difference I could see when dune installs is that the symlinks are converted to full files instead of being retained. This affects 4 .c files in litmus, as per the commit message.

[relokin]

The intent of this CI is to test with minimal versions. Is there a reason why this is not set to what version is promised to be sufficient?

[psafont]

Sorry I didn't copy the comment from the commit to the first message here, there's no lower version available which is compatible as well:

On the CI workflows, the version cannot be set to 3.11.0 as that version was unreleased, 3.12.1 is the lowest version published above 3.11

[relokin]

Since this PR dumps the minimum version for dune, we need wider consensus. cc: @fsestini, @maranget, @HadrienRenaud.

@psafont you might also want to update INSTALL.md

[psafont]

you might also want to update INSTALL.md

Should I also bump dune's required version in asllib/dune-project and asllib/aslspec/dune-project?

[HadrienRenaud]

you might also want to update INSTALL.md

Should I also bump dune's required version in asllib/dune-project and asllib/aslspec/dune-project?

Difficult to say without testing, but I guess 2 minors version of dune is not a lot so I'd say go ahead.

[fsestini]

Thanks @psafont. I like the general direction of this PR, however I'd like to expand on some of its implications a bit more.

One thing that the dune-install.sh and dune-uninstall.sh script did was to completely wipe the libdir directories before (re)installing/uninstalling. See this line in dune-install.sh:

rm -rf "${to}" && mkdir -p "${to}" && ( cd "${from}" && cp -r . "${to}" )

dune-uninstall.sh did a similar thing.

I believe the point of this is to prevent stale files from past installations to survive into the respective libdirs after a reinstall of herdtools7.

As far as I can tell, dune install just overwrites files, and dune uninstall does not delete whole directories (unless they are empty), so the behaviour described above is not preserved by this PR. For example, we can see that extra files that were previously in the libdir (e.g. from a previous installation) survive after a (re)install:

$ touch ~/.local/share/herdtools7/herd/extra-file
$ make install PREFIX=/Users/filses01/.local
$ ll ~/.local/share/herdtools7/herd | grep extra-file
-rw-r--r--@  1 filses01  staff      0  8 Jul 10:10 extra-file

Note that I don't disagree with this new behaviour in principle. In fact, I think (un)install scripts in general should not remove entire user directories unconditionally, and the behaviour proposed by this PR follows standard practice AFAICT.

So, again, I'm in favour of this change in principle, and I expect it to be harmless in practice as well, since our tools mostly look up specific filenames from the libdirs rather than enumerating or bulk-loading everything in there. However, I think it's an aspect worth pointing out to ensure we are all aware of the implications and are on board with it.

[psafont]

Just found a PR that's superseded by this one: #420

[psafont]

I've done a bit on investigation regarding the files types in the libdirs and how the tools use them to make sure that adding file doesn't interfere with how they work:

• Herd
  • .cat files: all cat files are used by name, both from other cat files and in herd/model.ml
    • Tested with a random .cat file added and running litmus tests, no changes observed.
  • .cfg files: herd reads a single configuration file, which can be overriden by using -conf
• jingle
  • .theme files are selected individually using the argument -theme
  • .call files are selected individually using the argument -call
  • .map files are selected individually using the argument -map
• litmus
  • Some C files and headers are included, I added a header in the _aarch64 directory with a conflicting type definition for ins_t which defined byinstruction.h, and proceeded to generate the source code, the expected, correct definition what placed in the .c file, while the conflicting one was not used. It didn't have any effect.
  • .awk files individually copied by the objUtils.ml, by name
  • .cfg files are selected using the argument -mach, individually
• tools
  • .cat file: the 2 existing ones don't seem to be references in tools/, uoaim had a parameter to load cat files with -cat

As far as I could see, changing the behaviour there doesn't change other that seeing a warning message when running make uninstall:

$ make uninstall PREFIX=/tmp/post
Error: Directory /tmp/post/share/herdtools7/litmus/_aarch64 is not empty,
cannot delete (ignoring).
Error: Directory /tmp/post/share/herdtools7/litmus is not empty, cannot
delete (ignoring).
Error: Directory /tmp/post/share/herdtools7/herd is not empty, cannot delete
(ignoring).

[fsestini]

Thanks a lot for looking into this @psafont . This LGTM.

[relokin]

LGTM! Thanks Pau. If you rebase on top of master, I will merge this PR.