Huge update of native code handling

[pkriens]

• Added Pardinus source code back into Alloy. Required to cleanup the native code.
• Update to the pardinus core for the SATFactory usage as identifier
• Added native code project
• Update to the native code handling
• Just removed some files to test that were used as examples
• Adaptions to the new native code handling
• Needed for eclipse

[pkriens]

This is a very large update :-( And this text is very technical.

I had been struggling with the native code for ever. The problem is that we have a list of solvers in A4Option and then we had a list in SATFactory. The SatSolver was used on the Alloy side to select a sat solver and this was then magically matched somewhere by name. It was basically all over the place. Then the native code was a mess. There was lots of commented platforms but they were still in the native code. Then the arm64 of MacOS was not in there at all. Also found out that the windows executables were 32 bit and did not run on windows anymore.

From one thing came the other ... I finally decided that we needed to make changes to the Pardinus code since it held the SATFactory. Since this was moved out in 6, I moved it back in. If this works, it can go back to its original. The basic changes to the Pardinus code are very limited. The SATFactory has been thoroughly updated and the native solver classes have been removed. Pardinus/KodKod has access to SAT4J by default but all native code handling has been removed to the native code project.

The changes to the SATFactory are that it is now usable as an identifier for the SAT solver. It provides a description of the sat solver, its properties, etc. There is no hardcoded list anymore. Anybody in the code can create a SATFactory and list it in the META-INF/services/kodkod.engine.satlab.SATFactory in his JAR. We find this through the standard Java ServiceLoader mechanism.

To support more mechanisms, the SATFactory getAllSolvers() methods also includes a standard list that can be updated anywhere in the code. This is used at startup to register external solvers. You can add a file ~/.alloy/extensions/sat that can specify the following properties:

• execute – The executable path. Must be absolute but may contain ~
• cnf – If set, defines the name of the cnf input file. If not set, a temp file is created
• maxsat – Set to anything indicate this is a maxsat
• prover – Set to anything indicate this is a prover
• description – A description of the solver

I was struggling with the electrod and I wonder if the extension mechanism might not be easier? Need some help in this.

The my magnus opus :-(

My goal was to be able to build all native code on Github actions. I've requested a signing service and then you need to build the whole product on the fly.

This is hard ... but I did it! We need to build on a Mac because linux & windows can be cross compiled but this seems impossible for mac. However, Github action has mac runners so that is not a big issue. The build now supports the following features:

• All supported native libraries are now in a forked repository on Alloytools. We create a branch alloy where we can patch the code if necessary and track any changes in the original. I used this to fix numerous warnings in the code.
• We checkout this repo from github before we build the binaries
• We actually generate the header files now from the native code classes, ensuring they match.
• For each native code, we have a special CMakeLists.txt file that uses cmake to build the product. It was impossible to get most of the available build support to get to work, especially Windows. With cmake it seems to work well. It means that we do not have to fiddle with the existing build system.
• The Mac binaries are created with the existing setup for amd64 and arm64
• The Linux/amd64 Windows/amd64 are build using dockercross

This was terrible work. And I am afraid we have some work left since the binaries need to be tested on all platforms.

I think I am going to be a researcher when I grow up so I do not have to much in native code :-)

[grayswandyr]

Looks like a lot of work indeed.

Since this was moved out in 6, I moved it back in. If this works, it can go back to its original.

Is this update is compatible with Pardinus being in its own repo without further burden on the Pardinus team? Or does moving Pardinus back to its repo incur some extra work for the team (such as handling a specific build configuration)? In the latter case, the added value for building would objectively result in a loss on the Pardinus side.

[pkriens]

I've come to the conclusion that the best solution is to manually sync the source code. Since the Pardinus repository had no updates for almost 2.5 years so it seems pretty stable. The source changes I needed are limited to basically SATSolver & NativeCode, manually synchronizing is infinitely easier than the struggling with two repositories. It is not my preferred way but sometimes it is the least bad.

This way the Pardinus team is completely independent of Alloytools.

[grayswandyr]

I think we're all more than happy that you cleaned up the handling of solvers. But concretely, technically:

• why is it impossible to use a Git submodule? What makes it problematic? Howcome modern tools can't handle a basic decoupling mechanism, by the way I would expect a fierce advocate of good architectural design likeyou to defend?
• if you only changed SATSolver & NativeCode, isn't it possible to leave the rest of the code in Pardinus?

[pkriens]

What is the problem doing the source sync? Then we're completely decoupled? It allows me to apply my build love to the code and it allows the Pardinus people to be 100% independent.

You have to trust me that the current setup really sucks for me. We can always revisit this in a year if the native code changes are stable.

[pkriens]

@grayswandyr @nmacedo we need to come to a conclusion here ... zoom/slack session?

[grayswandyr]

Yes, but I think we should ask at least Daniel and Aleks to participate, don't you think?

[pkriens]

Agree, you setup a meeting?

[aleksandarmilicevic]

I'm happy to review this, just ping me once:

• conflicts are resolved
• the build passes
• this PR is not a draft

Otherwise, 👍

[pkriens]

For the reviewers ... the build fails because it tries to commit to the master branch the native code. This PR needs to run once on master before that mechanism works. So ignore the native code branch

[pkriens]

@nmacedo and @aleksandarmilicevic time to do a review?

[nmacedo]

@pkriens still trying to process your impressive work on building the native solvers, but I'm a bit confused about having two native folders, one at the root of org.alloytools.pardinus.native (which is included in the resources but contains only a few binaries), and another at org.alloytools.pardinus.native/satsolvers that effectively contains all native solvers but doesn't seem to be included in the resources?

[pkriens]

I had to look again, at 65 my memory seems to slow down :-(

This should be corrected when I merge on master .. but that is hard to test before I got approval. When I build on native, it will run on a different Github Runner with Macos and build the natives. If this succeeds, I will commit the native directory to master.

I.e. the idea is to store the native executables in the master branch but I need this PR to work before I can get them on the master branch. It should all work out once this PR is approved. Chicken egg problem :-( Once it works once, it should be straightforward.

[grayswandyr]

@pkriens BTW how is the Electrod binary handled with your work? Is it procured and rebuilt automatically, or does it rely on a pre-compiled binary as before?

[pkriens]

I think the binary is handled as an external executable. I recall it was ocaml and they did not support generating arm64 binaries? Wasn't it also quite large?

[grayswandyr]

I think the binary is handled as an external executable.

Will it still be integrated inside the JAR?

I recall it was ocaml and they did not support generating arm64 binaries?

It is the best programming language in the world, yes :-) AFAIK it works under arm64.

Wasn't it also quite large?

Several megas per platform, I guess you may call this large when multiplied by the number of supported platforms.

[pkriens]

tomorrow I will work on Alloy ... got myself extremely neck deep in AI and starting to hate it. It is the absolute opposite of formal ... sorry for the delay