-
Notifications
You must be signed in to change notification settings - Fork 122
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Huge update of native code handling #218
Conversation
pkriens
commented
Jun 23, 2023
- 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
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
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:
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 :-) |
cfb3bd7
to
1f1a189
Compare
Looks like a lot of work indeed.
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. |
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. |
I think we're all more than happy that you cleaned up the handling of solvers. But concretely, technically:
|
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. |
@grayswandyr @nmacedo we need to come to a conclusion here ... zoom/slack session? |
Yes, but I think we should ask at least Daniel and Aleks to participate, don't you think? |
Agree, you setup a meeting? |
I'm happy to review this, just ping me once:
Otherwise, 👍 |
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 |
@nmacedo and @aleksandarmilicevic time to do a review? |
@pkriens still trying to process your impressive work on building the native solvers, but I'm a bit confused about having two |
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. |
@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? |
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? |
Will it still be integrated inside the JAR?
It is the best programming language in the world, yes :-) AFAIK it works under arm64.
Several megas per platform, I guess you may call this large when multiplied by the number of supported platforms. |
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 |