Skip to content
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

[CI] Add Github Actions workflow to run regression.sh #6

Merged
merged 2 commits into from
Mar 3, 2024

Conversation

jcreedcmu
Copy link
Collaborator

A docker image built from https://github.com/jcreedcmu/docker-mlton is available as jcreed/mlton-twelf-ci:latest on Docker Hub. It contains the MLton release binaries, and a script placed in /usr/bin/svnversion that actually just asks for the current git revision since we live in the present time and no longer use stone tools. This is enough for TEST/regression.sh to successfully run.

In passing, tweaked the bash syntax of that regression script, and reduced chatter in the warnings generated by MLton compilation of twelf, presumably due to the evolution of the semantics of default-ann 'nonexhaustiveMatch ignore' in the intervening years.

A docker image built from https://github.com/jcreedcmu/docker-mlton is
available as
[jcreed/mlton-twelf-ci:latest](https://hub.docker.com/repository/docker/jcreed/mlton-twelf-ci/general)
on Docker Hub. It contains the MLton release binaries, and a script
placed in `/usr/bin/svnversion` that actually just asks for the
current git revision since we live in the present time and no longer
use stone tools. This is enough for `TEST/regression.sh` to
successfully run.

In passing, tweaked the bash syntax of that regression script, and
reduced chatter in the warnings generated by MLton compilation of
twelf, presumably due to the evolution of the semantics of
`default-ann 'nonexhaustiveMatch ignore'` in the intervening years.
Copy link
Member

@robsimmons robsimmons left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

love to see it

@jcreedcmu jcreedcmu merged commit 7cc338a into master Mar 3, 2024
1 check passed
@robsimmons robsimmons deleted the jcreed/ci-test-experiment branch March 4, 2024 14:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants