Updated Docker CI workflow with SMT solvers (HolSmt)

[binghe]

Hi,

I have now updated the Docker image binghelisp/hol-dev:latest with the following SMT solvers installed:

• Z3 2.19
• Z3 2.19.1
• Z3 4.12.4 (latest)
• Yices 1.0.40
• CVC5 (latest)

This present PR contains the original Docker definitions, and I have already pushed the new Docker images to my binghelisp/hol-dev repository. Then 3 GitHub workflows are updated to actually use the new features provided by the updated Docker images.

The previous Docker image without these extra software, is now preserved as Docker image binghelisp/hol-dev:base. For the CI tests of PRs and new commits on develop, I put Z3 2.19 (with proof logging) and CVC5 by default. And for the manual tests described by the self-runner.yml workflow, various solvers and versions can be chosen (But notice that in arm64 Linux there's only Z3 4.12.4 available.)

Furthermore, I have updated HolSmt's code to allow environment variables HOL4_Z3_EXECUTABLE, etc. to be set to "" (empty string) to disable the related solvers. Previously HolSmt only detects the existence of these environment variables and call them as executions even the file name is empty. The changes here will make the Docker image design easier for switchable SMT solvers.

Chun

[someplaceguy]

Awesome, thanks!

[someplaceguy]

It would be very useful to find out which version of each solver has been used for the tests, just by looking at the CI logs.

This would be especially useful for debugging / troubleshooting purposes and for keeping the HolSmt documentation updated regarding which SMT solver versions have been tested.

I've downloaded the CI log archive for this PR but couldn't find any string in the logs that shows which version of Z3 or CVC5 is actually being used for the self-tests (presumably because it's downloading a Docker image/snapshot with the solvers already installed?).

So to that end, I was wondering if we could add a few commands like the following:

RUN echo "Using Z3 solver: `${HOL4_Z3_EXECUTABLE} --version`"
RUN echo "Using CVC solver: `${HOL4_CVC_EXECUTABLE} --version`"
RUN echo "Using Yices solver: `${HOL4_YICES_EXECUTABLE} --version`"

Perhaps this could be added just before RUN ${SML} < tools/smart-configure.sml, for example.

Disclaimer: I only have superficial knowledge of Docker so I'm not entirely sure if my suggestion would work as-is...

[binghe]

Now

It would be very useful to find out which version of each solver has been used for the tests, just by looking at the CI logs.

This would be especially useful for debugging / troubleshooting purposes and for keeping the HolSmt documentation updated regarding which SMT solver versions have been tested.

I've downloaded the CI log archive for this PR but couldn't find any string in the logs that shows which version of Z3 or CVC5 is actually being used for the self-tests (presumably because it's downloading a Docker image/snapshot with the solvers already installed?).

So to that end, I was wondering if we could add a few commands like the following:

RUN echo "Using Z3 solver: `${HOL4_Z3_EXECUTABLE} --version`"
RUN echo "Using CVC solver: `${HOL4_CVC_EXECUTABLE} --version`"
RUN echo "Using Yices solver: `${HOL4_YICES_EXECUTABLE} --version`"

Perhaps this could be added just before RUN ${SML} < tools/smart-configure.sml, for example.

Disclaimer: I only have superficial knowledge of Docker so I'm not entirely sure if my suggestion would work as-is...

Now you can see the solvers' version information from the CI build log:

[3/9] COPY --link . .
#11 merging
#11 merging 0.6s done
#11 DONE 1.7s
#12 [4/9] RUN if [ "" != "2.19" ]; then     echo "Using Z3 solver: `/ML/z3-2.19/bin/z3 -version`"; fi
#12 0.062 Using Z3 solver: Z3 version 2.19
#12 DONE 0.1s
#13 [5/9] RUN if [ "" != "5" ]; then     echo "Using CVC solver: `/ML/cvc5-Linux --version | head -1`"; fi
#13 0.064 Using CVC solver: This is cvc5 version 1.1.0 [git tag 1.1.0 branch HEAD]
#13 DONE 0.1s
#14 [6/9] RUN if [ "" != "${YICES_VERSION}" ]; then     echo "Using Yices solver: ` --version`"; fi
#14 DONE 0.1s

[someplaceguy]

Perfect, thank you!

[mn200]

Thanks for all this work!