search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
440 stars 40 forks source link

prepare the docker image for v0.6.0 #100

Closed konnov closed 4 years ago

konnov commented 4 years ago

The image can be pulled with docker pull apalache/mc

lemmy commented 4 years ago

Inside the docker image, what is the path to apalache-mc?

Background: https://github.com/lemmy/BlockingQueue/tree/apalache can be launched in the browser where it opens a TLA+ IDE based on the vscode-tlaplus extension and the apalache/mc docker image. However, I cannot find apalache-mc.

konnov commented 4 years ago

It should be in /opt/apalache/bin.

lemmy commented 4 years ago 
gitpod ~ $ /opt/apalache/bin/apalache-mc 
# Tool home: /opt/apalache
# Package:   /opt/apalache/mod-distribution/target/apalache-pkg-0.6.0-RELEASE-full.jar
# JVM args: -Xmx4096m -Djava.library.path=/opt/apalache/3rdparty/lib
#
/opt/apalache/bin/apalache-mc: line 57: java: command not found

If the docker image would come with Java, z3 in LIBRARY_PATH, and /opt/apalache/bin in PATH, one could run apalache in a browser.

konnov commented 4 years ago

Works for me here:

$ docker pull apalache/mc
Using default tag: latest
latest: Pulling from apalache/mc
Digest: sha256:0fcd327bfe951899dd6e959f2d3b276be9180058b22704ba3f04c01a1d0c6077
Status: Image is up to date for apalache/mc:latest
docker.io/apalache/mc:latest

$ docker run -it --entrypoint /bin/bash apalache/mc
root@1b72eea3091f:/opt/apalache# ls /opt/apalache/bin/
apalache-mc  run-in-docker-container
konnov commented 4 years ago

I see, the only problem is that apalache-mc is not available in PATH. I will fix that.

lemmy commented 4 years ago

Is it possible that your setup uses a JVM that it outside the docker image? With this browser thing, it seems we are "inside" the image.

konnov commented 4 years ago

In the docker image:

root@1b72eea3091f:/opt/apalache# java -version
Picked up _JAVA_OPTIONS: -Djdk.net.URLClassPath.disableClassPathURLCheck=true
openjdk version "1.8.0_242"
OpenJDK Runtime Environment (build 1.8.0_242-b08)
OpenJDK 64-Bit Server VM (build 25.242-b08, mixed mode)

in my shell:

$ java -version
java version "1.8.0_172"
Java(TM) SE Runtime Environment (build 1.8.0_172-b11)
Java HotSpot(TM) 64-Bit Server VM (build 25.172-b11, mixed mode)
lemmy commented 4 years ago 
gitpod /opt/apalache $ git log
commit 25bfb2d2c2a8a7dbf6a23305787d9c36859534b2 (HEAD -> master, tag: v0.6.0, origin/master, origin/HEAD)
Author: Igor Konnov <igor@interchain.io>
Date:   Fri Feb 14 14:09:31 2020 +0100

    the release notes

gitpod ~ $ dpkg -l |grep java
gitpod ~ $ dpkg -l |grep oracle
gitpod ~ $ dpkg -l
Desired=Unknown/Install/Remove/Purge/Hold
| Status=Not/Inst/Conf-files/Unpacked/halF-conf/Half-inst/trig-aWait/Trig-pend
|/ Err?=(none)/Reinst-required (Status,Err: uppercase=bad)
||/ Name                       Version                     Architecture Description
+++-==========================-===========================-============-===============================================================================
ii  adduser                    3.118                       all          add and remove users and groups
ii  apt                        1.8.2                       amd64        commandline package manager
ii  base-files                 10.3+deb10u2                amd64        Debian base system miscellaneous files
ii  base-passwd                3.5.46                      amd64        Debian base system master password and group files
ii  bash                       5.0-4                       amd64        GNU Bourne Again SHell
ii  bash-completion            1:2.8-6                     all          programmable completion for the bash shell
ii  binutils                   2.31.1-16                   amd64        GNU assembler, linker and binary utilities
ii  binutils-common:amd64      2.31.1-16                   amd64        Common files for the GNU assembler, linker and binary utilities
ii  binutils-x86-64-linux-gnu  2.31.1-16                   amd64        GNU binary utilities, for x86-64-linux-gnu target
ii  bsdutils                   1:2.33.1-0.1                amd64        basic utilities from 4.4BSD-Lite
ii  bzip2                      1.0.6-9.2~deb10u1           amd64        high-quality block-sorting file compressor - utilities
ii  ca-certificates            20190110                    all          Common CA certificates
ii  coreutils                  8.30-3                      amd64        GNU core utilities
ii  cpp                        4:8.3.0-1                   amd64        GNU C preprocessor (cpp)
ii  cpp-8                      8.3.0-6                     amd64        GNU C preprocessor
ii  curl                       7.64.0-4                    amd64        command line tool for transferring data with URL syntax
ii  dash                       0.5.10.2-5                  amd64        POSIX-compliant shell
ii  debconf                    1.5.71                      all          Debian configuration management system
ii  debian-archive-keyring     2019.1                      all          GnuPG archive keys of the Debian archive
ii  debianutils                4.8.6.1                     amd64        Miscellaneous utilities specific to Debian
ii  diffutils                  1:3.7-3                     amd64        File comparison utilities
ii  dpkg                       1.19.7                      amd64        Debian package management system
ii  e2fsprogs                  1.44.5-1+deb10u2            amd64        ext2/ext3/ext4 file system utilities
ii  fdisk                      2.33.1-0.1                  amd64        collection of partitioning utilities
ii  file                       1:5.35-4+deb10u1            amd64        Recognize the type of data in a file using "magic" numbers
ii  findutils                  4.6.0+git+20190209-2        amd64        utilities for finding files--find, xargs
ii  g++                        4:8.3.0-1                   amd64        GNU C++ compiler
ii  g++-8                      8.3.0-6                     amd64        GNU C++ compiler
ii  gcc                        4:8.3.0-1                   amd64        GNU C compiler
ii  gcc-8                      8.3.0-6                     amd64        GNU C compiler
ii  gcc-8-base:amd64           8.3.0-6                     amd64        GCC, the GNU Compiler Collection (base package)
ii  git                        1:2.20.1-2+deb10u1          amd64        fast, scalable, distributed revision control system
ii  git-man                    1:2.20.1-2+deb10u1          all          fast, scalable, distributed revision control system (manual pages)
ii  gpgv                       2.2.12-1+deb10u1            amd64        GNU privacy guard - signature verification tool
ii  grep                       3.3-1                       amd64        GNU grep, egrep and fgrep
ii  gzip                       1.9-3                       amd64        GNU compression utilities
ii  hostname                   3.21                        amd64        utility to set/show the host name or domain name
ii  init-system-helpers        1.56+nmu1                   all          helper tools for all init systems
ii  krb5-locales               1.17-3                      all          internationalization support for MIT Kerberos
ii  less                       487-0.1+b1                  amd64        pager program similar to more
ii  libacl1:amd64              2.2.53-4                    amd64        access control list - shared library
ii  libapt-pkg5.0:amd64        1.8.2                       amd64        package management runtime library
ii  libasan5:amd64             8.3.0-6                     amd64        AddressSanitizer -- a fast memory error detector
ii  libatomic1:amd64           8.3.0-6                     amd64        support library providing __atomic built-in functions
ii  libattr1:amd64             1:2.4.48-4                  amd64        extended attribute handling - shared library
ii  libaudit-common            1:2.8.4-3                   all          Dynamic library for security auditing - common files
ii  libaudit1:amd64            1:2.8.4-3                   amd64        Dynamic library for security auditing
ii  libbinutils:amd64          2.31.1-16                   amd64        GNU binary utilities (private shared library)
ii  libblkid1:amd64            2.33.1-0.1                  amd64        block device ID library
ii  libbsd0:amd64              0.9.1-2                     amd64        utility functions from BSD systems - shared library
ii  libbz2-1.0:amd64           1.0.6-9.2~deb10u1           amd64        high-quality block-sorting file compressor library - runtime
ii  libc-bin                   2.28-10                     amd64        GNU C Library: Binaries
ii  libc-dev-bin               2.28-10                     amd64        GNU C Library: Development binaries
ii  libc6:amd64                2.28-10                     amd64        GNU C Library: Shared libraries
ii  libc6-dev:amd64            2.28-10                     amd64        GNU C Library: Development Libraries and Header Files
ii  libcap-ng0:amd64           0.7.9-2                     amd64        An alternate POSIX capabilities library
ii  libcc1-0:amd64             8.3.0-6                     amd64        GCC cc1 plugin for GDB
ii  libcom-err2:amd64          1.44.5-1+deb10u2            amd64        common error description library
ii  libcurl3-gnutls:amd64      7.64.0-4                    amd64        easy-to-use client-side URL transfer library (GnuTLS flavour)
ii  libcurl4:amd64             7.64.0-4                    amd64        easy-to-use client-side URL transfer library (OpenSSL flavour)
ii  libdb5.3:amd64             5.3.28+dfsg1-0.5            amd64        Berkeley v5.3 Database Libraries [runtime]
ii  libdebconfclient0:amd64    0.249                       amd64        Debian Configuration Management System (C-implementation library)
ii  libedit2:amd64             3.1-20181209-1              amd64        BSD editline and history libraries
ii  liberror-perl              0.17027-2                   all          Perl module for error/exception handling in an OO-ish way
ii  libexpat1:amd64            2.2.6-2+deb10u1             amd64        XML parsing C library - runtime library
ii  libext2fs2:amd64           1.44.5-1+deb10u2            amd64        ext2/ext3/ext4 file system libraries
ii  libfdisk1:amd64            2.33.1-0.1                  amd64        fdisk partitioning library
ii  libffi6:amd64              3.2.1-9                     amd64        Foreign Function Interface library runtime
ii  libgcc-8-dev:amd64         8.3.0-6                     amd64        GCC support library (development files)
ii  libgcc1:amd64              1:8.3.0-6                   amd64        GCC support library
ii  libgcrypt20:amd64          1.8.4-5                     amd64        LGPL Crypto library - runtime library
ii  libgdbm-compat4:amd64      1.18.1-4                    amd64        GNU dbm database routines (legacy support runtime version) 
ii  libgdbm6:amd64             1.18.1-4                    amd64        GNU dbm database routines (runtime version) 
ii  libgmp10:amd64             2:6.1.2+dfsg-4              amd64        Multiprecision arithmetic library
ii  libgnutls30:amd64          3.6.7-4                     amd64        GNU TLS library - main runtime library
ii  libgomp1:amd64             8.3.0-6                     amd64        GCC OpenMP (GOMP) support library
ii  libgpg-error0:amd64        1.35-1                      amd64        GnuPG development runtime library
ii  libgpm2:amd64              1.20.7-5                    amd64        General Purpose Mouse - shared library
ii  libgssapi-krb5-2:amd64     1.17-3                      amd64        MIT Kerberos runtime libraries - krb5 GSS-API Mechanism
ii  libhogweed4:amd64          3.4.1-1                     amd64        low level cryptographic library (public-key cryptos)
ii  libidn2-0:amd64            2.0.5-1                     amd64        Internationalized domain names (IDNA2008/TR46) library
ii  libisl19:amd64             0.20-2                      amd64        manipulating sets and relations of integer points bounded by linear constraints
ii  libitm1:amd64              8.3.0-6                     amd64        GNU Transactional Memory Library
ii  libk5crypto3:amd64         1.17-3                      amd64        MIT Kerberos runtime libraries - Crypto Library
ii  libkeyutils1:amd64         1.6-6                       amd64        Linux Key Management Utilities (library)
ii  libkrb5-3:amd64            1.17-3                      amd64        MIT Kerberos runtime libraries
ii  libkrb5support0:amd64      1.17-3                      amd64        MIT Kerberos runtime libraries - Support library
ii  libldap-2.4-2:amd64        2.4.47+dfsg-3+deb10u1       amd64        OpenLDAP libraries
ii  libldap-common             2.4.47+dfsg-3+deb10u1       all          OpenLDAP common files for libraries
ii  liblsan0:amd64             8.3.0-6                     amd64        LeakSanitizer -- a memory leak detector (runtime)
ii  liblz4-1:amd64             1.8.3-1                     amd64        Fast LZ compression algorithm library - runtime
ii  liblzma5:amd64             5.2.4-1                     amd64        XZ-format compression library
ii  libmagic-mgc               1:5.35-4+deb10u1            amd64        File type determination library using "magic" numbers (compiled magic file)
ii  libmagic1:amd64            1:5.35-4+deb10u1            amd64        Recognize the type of data in a file using "magic" numbers - library
ii  libmount1:amd64            2.33.1-0.1                  amd64        device mounting library
ii  libmpc3:amd64              1.1.0-1                     amd64        multiple precision complex floating-point library
ii  libmpfr6:amd64             4.0.2-1                     amd64        multiple precision floating-point computation
ii  libmpx2:amd64              8.3.0-6                     amd64        Intel memory protection extensions (runtime)
ii  libncurses6:amd64          6.1+20181013-2+deb10u2      amd64        shared libraries for terminal handling
ii  libncursesw6:amd64         6.1+20181013-2+deb10u2      amd64        shared libraries for terminal handling (wide character support)
ii  libnettle6:amd64           3.4.1-1                     amd64        low level cryptographic library (symmetric and one-way cryptos)
ii  libnghttp2-14:amd64        1.36.0-2+deb10u1            amd64        library implementing HTTP/2 protocol (shared library)
ii  libp11-kit0:amd64          0.23.15-2                   amd64        library for loading and coordinating access to PKCS#11 modules - runtime
ii  libpam-modules:amd64       1.3.1-5                     amd64        Pluggable Authentication Modules for PAM
ii  libpam-modules-bin         1.3.1-5                     amd64        Pluggable Authentication Modules for PAM - helper binaries
ii  libpam-runtime             1.3.1-5                     all          Runtime support for the PAM library
ii  libpam0g:amd64             1.3.1-5                     amd64        Pluggable Authentication Modules library
ii  libpcre2-8-0:amd64         10.32-5                     amd64        New Perl Compatible Regular Expression Library- 8 bit runtime files
ii  libpcre3:amd64             2:8.39-12                   amd64        Old Perl 5 Compatible Regular Expression Library - runtime files
ii  libperl5.28:amd64          5.28.1-6                    amd64        shared Perl library
ii  libprocps7:amd64           2:3.3.15-2                  amd64        library for accessing process information from /proc
ii  libpsl5:amd64              0.20.2-2                    amd64        Library for Public Suffix List (shared libraries)
ii  libpython-stdlib:amd64     2.7.16-1                    amd64        interactive high-level object-oriented language (Python2)
ii  libpython2-stdlib:amd64    2.7.16-1                    amd64        interactive high-level object-oriented language (Python2)
ii  libpython2.7-minimal:amd64 2.7.16-2+deb10u1            amd64        Minimal subset of the Python language (version 2.7)
ii  libpython2.7-stdlib:amd64  2.7.16-2+deb10u1            amd64        Interactive high-level object-oriented language (standard library, version 2.7)
ii  libquadmath0:amd64         8.3.0-6                     amd64        GCC Quad-Precision Math Library
ii  libreadline7:amd64         7.0-5                       amd64        GNU readline and history libraries, run-time libraries
ii  librtmp1:amd64             2.4+20151223.gitfa8646d.1-2 amd64        toolkit for RTMP streams (shared library)
ii  libsasl2-2:amd64           2.1.27+dfsg-1+deb10u1       amd64        Cyrus SASL - authentication abstraction library
ii  libsasl2-modules:amd64     2.1.27+dfsg-1+deb10u1       amd64        Cyrus SASL - pluggable authentication modules
ii  libsasl2-modules-db:amd64  2.1.27+dfsg-1+deb10u1       amd64        Cyrus SASL - pluggable authentication modules (DB)
ii  libseccomp2:amd64          2.3.3-4                     amd64        high level interface to Linux seccomp filter
ii  libselinux1:amd64          2.8-1+b1                    amd64        SELinux runtime shared libraries
ii  libsemanage-common         2.8-2                       all          Common files for SELinux policy management libraries
ii  libsemanage1:amd64         2.8-2                       amd64        SELinux policy management library
ii  libsepol1:amd64            2.8-1                       amd64        SELinux library for manipulating binary security policies
ii  libsmartcols1:amd64        2.33.1-0.1                  amd64        smart column output alignment library
ii  libsqlite3-0:amd64         3.27.2-3                    amd64        SQLite 3 shared library
ii  libss2:amd64               1.44.5-1+deb10u2            amd64        command-line interface parsing library
ii  libssh2-1:amd64            1.8.0-2.1                   amd64        SSH2 client-side library
ii  libssl1.1:amd64            1.1.1d-0+deb10u2            amd64        Secure Sockets Layer toolkit - shared libraries
ii  libstdc++-8-dev:amd64      8.3.0-6                     amd64        GNU Standard C++ Library v3 (development files)
ii  libstdc++6:amd64           8.3.0-6                     amd64        GNU Standard C++ Library v3
ii  libsystemd0:amd64          241-7~deb10u2               amd64        systemd utility library
ii  libtasn1-6:amd64           4.13-3                      amd64        Manage ASN.1 structures (runtime)
ii  libtinfo6:amd64            6.1+20181013-2+deb10u2      amd64        shared low-level terminfo library for terminal handling
ii  libtsan0:amd64             8.3.0-6                     amd64        ThreadSanitizer -- a Valgrind-based detector of data races (runtime)
ii  libubsan1:amd64            8.3.0-6                     amd64        UBSan -- undefined behaviour sanitizer (runtime)
ii  libudev1:amd64             241-7~deb10u2               amd64        libudev shared library
ii  libunistring2:amd64        0.9.10-1                    amd64        Unicode string library for C
ii  libuuid1:amd64             2.33.1-0.1                  amd64        Universally Unique ID library
ii  libx11-6:amd64             2:1.6.7-1                   amd64        X11 client-side library
ii  libx11-data                2:1.6.7-1                   all          X11 client-side library
ii  libxau6:amd64              1:1.0.8-1+b2                amd64        X11 authorisation library
ii  libxcb1:amd64              1.13.1-2                    amd64        X C Binding
ii  libxdmcp6:amd64            1:1.1.2-3                   amd64        X11 Display Manager Control Protocol library
ii  libxext6:amd64             2:1.3.3-1+b2                amd64        X11 miscellaneous extension library
ii  libxmuu1:amd64             2:1.1.2-2+b3                amd64        X11 miscellaneous micro-utility library
ii  libzstd1:amd64             1.3.8+dfsg-3                amd64        fast lossless compression algorithm
ii  linux-libc-dev:amd64       4.19.98-1                   amd64        Linux support headers for userspace development
ii  login                      1:4.5-1.1                   amd64        system login tools
ii  lsb-base                   10.2019051400               all          Linux Standard Base init script functionality
ii  make                       4.2.1-1.2                   amd64        utility for directing compilation
ii  manpages                   4.16-2                      all          Manual pages about using a GNU/Linux system
ii  manpages-dev               4.16-2                      all          Manual pages about using GNU/Linux for development
ii  mawk                       1.3.3-17+b3                 amd64        a pattern scanning and text processing language
ii  mime-support               3.62                        all          MIME files 'mime.types' & 'mailcap', and support programs
ii  mount                      2.33.1-0.1                  amd64        tools for mounting and manipulating filesystems
ii  ncurses-base               6.1+20181013-2+deb10u2      all          basic terminal type definitions
ii  ncurses-bin                6.1+20181013-2+deb10u2      amd64        terminal-related programs and man pages
ii  netbase                    5.6                         all          Basic TCP/IP networking system
ii  openssh-client             1:7.9p1-10+deb10u2          amd64        secure shell (SSH) client, for secure access to remote machines
ii  openssl                    1.1.1d-0+deb10u2            amd64        Secure Sockets Layer toolkit - cryptographic utility
ii  p11-kit                    0.23.15-2                   amd64        p11-glue utilities
ii  p11-kit-modules:amd64      0.23.15-2                   amd64        p11-glue proxy and trust modules
ii  passwd                     1:4.5-1.1                   amd64        change and administer password and group data
ii  patch                      2.7.6-3+deb10u1             amd64        Apply a diff file to an original
ii  perl                       5.28.1-6                    amd64        Larry Wall's Practical Extraction and Report Language
ii  perl-base                  5.28.1-6                    amd64        minimal Perl system
ii  perl-modules-5.28          5.28.1-6                    all          Core Perl modules
ii  procps                     2:3.3.15-2                  amd64        /proc file system utilities
ii  psmisc                     23.2-1                      amd64        utilities that use the proc file system
ii  publicsuffix               20190415.1030-1             all          accurate, machine-readable list of domain name suffixes
ii  python                     2.7.16-1                    amd64        interactive high-level object-oriented language (Python2 version)
ii  python-minimal             2.7.16-1                    amd64        minimal subset of the Python2 language
ii  python2                    2.7.16-1                    amd64        interactive high-level object-oriented language (Python2 version)
ii  python2-minimal            2.7.16-1                    amd64        minimal subset of the Python2 language
ii  python2.7                  2.7.16-2+deb10u1            amd64        Interactive high-level object-oriented language (version 2.7)
ii  python2.7-minimal          2.7.16-2+deb10u1            amd64        Minimal subset of the Python language (version 2.7)
ii  readline-common            7.0-5                       all          GNU readline and history libraries, common files
ii  sed                        4.7-1                       amd64        GNU stream editor for filtering/transforming text
ii  sysvinit-utils             2.93-8                      amd64        System-V-like utilities
ii  tar                        1.30+dfsg-6                 amd64        GNU version of the tar archiving utility
ii  tzdata                     2019c-0+deb10u1             all          time zone and daylight-saving time data
ii  util-linux                 2.33.1-0.1                  amd64        miscellaneous system utilities
ii  vim                        2:8.1.0875-5                amd64        Vi IMproved - enhanced vi editor
ii  vim-common                 2:8.1.0875-5                all          Vi IMproved - Common files
ii  vim-runtime                2:8.1.0875-5                all          Vi IMproved - Runtime files
ii  wget                       1.20.1-1.1                  amd64        retrieves files from the web
ii  xauth                      1:1.0.10-1                  amd64        X authentication utility
ii  xxd                        2:8.1.0875-5                amd64        tool to make (or reverse) a hex dump
ii  xz-utils                   5.2.4-1                     amd64        XZ-format compression utilities
ii  zlib1g:amd64               1:1.2.11.dfsg-1             amd64        compression library - runtime
gitpod ~ $ which java
gitpod ~ $
konnov commented 4 years ago

@andrey-kuprianov will publish the new docker image. It takes about 30 minutes though. I am not sure about what gitpod is pulling. I have just cleaned the docker images and did docker pull apalache/mc

$ docker run -it --entrypoint /bin/bash apalache/mc
root@dfa22aa3d972:/opt/apalache# java -version
Picked up _JAVA_OPTIONS: -Djdk.net.URLClassPath.disableClassPathURLCheck=true
openjdk version "1.8.0_242"
OpenJDK Runtime Environment (build 1.8.0_242-b08)
OpenJDK 64-Bit Server VM (build 25.242-b08, mixed mode)
root@dfa22aa3d972:/opt/apalache# which java
/usr/local/openjdk-8/bin/java
lemmy commented 4 years ago

I assumed the docker image would use zulu that gets installed as a regular debian package. From https://hub.docker.com/layers/apalache/mc/0.6.0/images/sha256-0fcd327bfe951899dd6e959f2d3b276be9180058b22704ba3f04c01a1d0c6077?context=explore I figured that you manually install Java to /usr/local/openjdk-8/.

In other words, gitpod pulls the correct docker image.

konnov commented 4 years ago

We don't, but it gets pulled with maven :-)

konnov commented 4 years ago

The fresh docker image apalache/mc has PATH set to /opt/apalache/bin:$PATH

lemmy commented 4 years ago

Could you set path to PATH=/usr/local/openjdk-8/bin/:/opt/apalache/bin/:$PATH?

konnov commented 4 years ago

It is actually set like this:

/opt/apalache/bin:/usr/local/openjdk-8/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
lemmy commented 4 years ago

Apalache in a browser (zero install): https://gitpod.io/#https://github.com/lemmy/BlockingQueue/tree/apalache

apalachegitpod

konnov commented 4 years ago

That is amazing! It did not work out of the box for me, still had to export PATH=/opt/apalache/bin:/usr/local/jdk....

konnov commented 4 years ago

Are you going to publish this work somewhere? It is really closing the last mile for the non-experts.

lemmy commented 4 years ago

Glad that you like it. The work is already public and other GitHub repositories can be made to work simply by adding a .gitpod.yml to the root of the repo. A user then only has to open https://gitpod.io/#https://github.com/konnov/ATLA+SpecRepo.

About PATH: Do you see this in the Terminal after launch?

gitpod /workspace/BlockingQueue $ HISTFILE=/workspace/.gitpod/cmd-2 history -r; {
> export PATH=/usr/local/openjdk-8/bin/:/opt/apalache/bin/:$PATH
> }

If not, I assume https://github.com/lemmy/BlockingQueue/blob/4ff1ee110def780f38ce7b8fa10673fbba1aed04/.gitpod.yml#L10 worked for me, because gitpod remembers PATH for my account specifically.

By now, I've tried all kinds of workarounds to set PATH. What should work is for the docker image apalache/mc to create symlinks to apalache-mc and java in /usr/local/bin. Adding a symlink for java might even fix the vscode extension that fails to launch TLC right now.

konnov commented 4 years ago

Andrey has updated PATH, so it looks like that in Dockerfile:

ENV PATH="/usr/local/openjdk-8/bin/:/opt/apalache/bin:${PATH}"

As for the symlinks, it looks like Docker does not support symlinks. Let's think of a solution that works for all of us.

lemmy commented 4 years ago

I just tried with a fresh Github account and PATH correctly includes /usr/local/openjdk-8/bin/:/opt/apalache/bin. In other words, everything appears to work out-of-the-box.