-
Notifications
You must be signed in to change notification settings - Fork 47
Add packaging support for Docker images #739
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
base: dev
Are you sure you want to change the base?
Conversation
|
Currently, the Ultimate tools are built with individual build calls, and the appropriate configurations (toolchain and settings files) are still missing in the respective Docker images. It would be advantageous if the complete build of the Docker images would be based on the A new separation of functionality could look like this:
The separation introduces the |
|
That's a very good idea. I also like your Dockerfile, in particular the use of dockerize! |
88c171b to
73aa7e5
Compare
The patch for the Jekyll installation is no longer necessary since the issue was fixed by updating Jekyll in commit c0f9255.
This change introduces a new makeBuild.sh script that builds all Ultimate products and packages the products with the required configurations (toolchain and settings files), additional programs and files like solvers or licenses. This script is then used in the existing makeFresh.sh script for the common build steps to avoid duplicate script code. The functionality of the makeFresh.sh script remains unchanged.
73aa7e5 to
27e6a0f
Compare
ec622b4 to
1523f5a
Compare
1523f5a to
a221748
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Very cool changes!
I added some minor comments, and have two things:
Use "real" webserver
I would like to avoid using the Jekyll webserver for the frontend. Could you just use nginx as base?
Our current frontend at https://ultimate-pa.org does the following.
services:
frontend:
image: nginx:latest
volumes:
- /mnt/shared/ultimate-pa/config/nginx/conf.d:/etc/nginx/conf.d
- /mnt/shared/ultimate-pa/config/nginx/nginx.conf:/etc/nginx/nginx.conf
- /mnt/shared/ultimate-pa/frontend:/www/frontend
- /mnt/shared/ultimate-pa/config/frontend/config.js:/www/frontend/config/config.j
where /mnt/shared/ultimate-pa/frontend is the static website, config.js the config you would expect, /mnt/shared/ultimate-pa/config/nginx/nginx.conf is default, and /mnt/shared/ultimate-pa/config/nginx/conf.d/default.conf is default except specifying the frontend folder:
server {
listen 80;
listen [::]:80;
server_name localhost;
location / {
root /www/frontend;
index index.html index.htm;
}
error_page 500 502 503 504 /50x.html;
location = /50x.html {
root /usr/share/nginx/html;
}
error_page 404 /404.html;
location /404.html {
root /www/frontend;
internal;
}
}
Check windows build
I tried running ./makeFresh.sh as usual, and got at the end:
Archive Ultimate Debug UI [linux]
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
Not enough arguments supplied -- use arguments in the following order
1. the toolname
2. the launcher name
3. the maximum heap memory size
4. the maximum stack memory size
5. 'linux' or 'win32' for the target platform
But everything else worked as expected
| # default entry point to serve the Ultimate web frontend | ||
| ENTRYPOINT dockerize -template "config.js.tpl:js/webinterface/config.js" \ | ||
| bundle exec jekyll serve --host "${ULTIMATE_FRONTEND_HOST}" \ | ||
| --port "${ULTIMATE_FRONTEND_PORT}" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hm, why not build the frontend with jekyll and serve it with a "real" webserver? I was at least under the impression that jekyll serve is only used for debugging/designing a website, not really for production use.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I created the Docker image of the Web frontend for development purposes. Here, jekyll serve offers an automatic rebuild and reload mechanism, which makes it super easy to debug and extend the frontend.
This is obviously not suitable for a productive Docker setup. In this case, you would probably be better off using a decent Web server, like your proposed nginx, and a powerful proxy server, like Traefik.
We could create a second Docker image of the Web frontend for production purposes. What do you think?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, that makes sense. Perhaps a comment in the README would be nice so that we remember why it is like it is :)
And of course, a second variant with nginx would be appreciated, then I would switch our current setup over to that.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this could now become a function in makeFresh -- which could also be somewhat simpler then. In particular, now that packaging is done before and this only names the zip and actually creates it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good idea! The script has become very small now. It's really not worth a script anymore.
…ucts
The standard memory sizes of the Java Runtime for Ultimate products are
uniformly set to the following values:
- Initial heap memory size: 2M
- Maximum heap memory size: 4G
- Maximum stack memory size: 1M
If other memory sizes are required, these can be configured for each
build of Ultimate products. The Ultimate products for the SV-COMP should
be built with the following settings:
./makeBuild.sh -i 2M -m 15G -s 1M
On the other hand, the ReqCheck product for analyzing large requirement
sets should be built with the following settings:
./makeBuild.sh -i 2M -m 100G -s 4M
| printf %s "$next" | ||
| } | ||
|
|
||
| semver_compare() { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I just tried running makeFresh.sh, but it just showed the build splashscreen and exited silently.
I checked and it turned out that javac --version produced javac 24, which should be >= 21.
After I used update-alternatives to change javac to 21, the build worked as expected.
Therefore, I think there is some issue here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You're right. The version comparison should support that.
The Docker packaging support allows to build Docker images for all Ultimate tools. The images are based on Alpine Linux to ensure a minimal footprint. The build is based on a multi-stage process where temporary build artifacts are discarded and not included in the final Docker images. Each Ultimate tool now has its own dedicated Docker image. Additionally, the WebBackend can be automatically configured through docker-compose environment files to simplify the configuration and deployment of the Web service.