sireum / kekinian

Sireum: A High Assurance System Engineering Platform
http://sireum.org
BSD 2-Clause "Simplified" License
9 stars 2 forks source link

[bug] Installing HAMR in Docker seems to stall #4

Closed podhrmic closed 3 months ago

podhrmic commented 4 months ago

When following the installation instructions from here and attempting to install FMIDE in a Ubuntu:22.04 docker container, the install seems to stall at bin/install/fmide.cmd:

Sireum-dev IVE can now be launched by running /opt/Sireum/bin/linux/idea/bin/IVE.sh
Java Development Kit (JDK) is available at /opt/Sireum/bin/linux/java
Scala is available at /opt/Sireum/bin/scala
Removing intermediate container f61440012bb1
 ---> 2a039dee7028
Step 9/9 : RUN bin/install/fmide.cmd
 ---> Running in 5a6663e40370
Installing FMIDE (this will take a while) ...
# seems to hang up - no CPU activity, no updates for > 30min

Is it possible to install HAMR in a docker container, or is it not a supported/recommended way?

jasonbelt commented 4 months ago

Michal,

Yes, you can install FMIDE inside a docker container. You could try turning verbosity on to see where it's hanging (e.g. bin/install/fmide.cmd --verbose)

fyi, I just tried the installation instructions on an x86 Ubuntu 22.04 container on my M3 Mac (FMIDE isn't supported on ARM so I had to switch to x86 emulation). The FMIDE install did get stuck while trying to install the CASE plugins. I switched to a docker container on an actual x86 box and the install completed successfully so I'm guessing it's an issue with the emulation.

Below is what a successful installation looks like when verbosity is enabled.

...
This is used by the plugins to locate where Sireum is installed.
Installing com.rockwellcollins.atc.agree.feature.feature.group/2.9.1 OSATE plugin from http://ca-trustedsystems-dev-us-east-1.s3-website-us-east-1.amazonaws.com/p2/snapshots/agree/,https://raw.githubusercontent.com/loonwerks/AGREE-Updates/master
Installing com.rockwellcollins.atc.resolute.feature.feature.group/3.0.0 OSATE plugin from http://ca-trustedsystems-dev-us-east-1.s3-website-us-east-1.amazonaws.com/p2/snapshots/resolute/,https://raw.githubusercontent.com/loonwerks/Resolute-Updates/master
Installing com.collins.trustedsystems.briefcase.feature.feature.group/0.8.0 OSATE plugin from https://download.eclipse.org/releases/2021-03,http://ca-trustedsystems-dev-us-east-1.s3-website-us-east-1.amazonaws.com/p2/snapshots/briefcase/,https://raw.githubusercontent.com/loonwerks/BriefCASE-Updates/master
Installing org.sireum.aadl.osate.feature.feature.group/1.2023.11061541.f31948c OSATE plugin from https://raw.githubusercontent.com/sireum/osate-update-site/master
Installing org.sireum.aadl.gumbo.feature.feature.group/1.2024.4181415.5990efb OSATE plugin from https://raw.githubusercontent.com/sireum/aadl-gumbo-update-site/master
Installing org.sireum.aadl.osate.awas.feature.feature.group/1.2023.11061541.f31948c OSATE plugin from https://raw.githubusercontent.com/sireum/osate-update-site/master
Installing org.sireum.aadl.osate.hamr.feature.feature.group/1.2023.11061541.f31948c OSATE plugin from https://raw.githubusercontent.com/sireum/osate-update-site/master
Installing org.sireum.aadl.osate.cli.feature.feature.group/1.2023.11061541.f31948c OSATE plugin from https://raw.githubusercontent.com/sireum/osate-update-site/master
Installing org.sireum.aadl.osate.gumbo2air.feature.feature.group/1.2024.4181415.5990efb OSATE plugin from https://raw.githubusercontent.com/sireum/aadl-gumbo-update-site/master
Plugins successfully installed.
podhrmic commented 4 months ago

Thanks, that worked! I realized (perhaps too late) that HAMR seems to require X11 to be enabled, otherwise I am getting a display error:

root@51a6ce14290e:/opt/Sireum# bin/linux/fmide/fmide --version
Fmide: Cannot open display

Is it possible to run HAMR tools in Docker, or would you recommend we use a VM instead?

jasonbelt commented 4 months ago

It's actually OSATE/FMIDE that requires some way of displaying its GUI. You can run GUI applications from the container (e.g. here, but I'd probably opt for using a VM instead -- assuming that you don't want to install things natively.

fyi, HAMR can generate an AADL instance model from OSATE/FMIDE headlessly. E.g. we use this for our regression testing on Github, one of which runs inside a CAmkES docker container. However, if you're going through the HAMR tutorials then you will want to be able to launch OSATE/FMIDE's GUI (as well as IVE's).

podhrmic commented 4 months ago

Makes sense, thanks for the explanation!

github-actions[bot] commented 3 months ago

This issue is stale because it has been open for 30 days with no activity.