Publish Docker image + Example CI WF + Upload to dockerhub by F-WRunTime · Pull Request #516 · runtimeverification/mir-semantics

F-WRunTime · 2025-03-28T22:30:45Z

… bugs and challenge to fully isolate built dependencies into the src contained for packaging and installation deployiment.

Current problem:

Post installation of whl .cache/kdist- file is not available and hardcoded to look in ~/.cache/kdist-
This needs a generalized location or be installed to site-package swith the rest of the library files for python packaging to work as intended.
Unresolved understanding of where stable-mir-json artifacts need to be stored / referenced for kmir prove
Published a single docker image from manual built image to produce an alias poetry-kmir usable image within CI, but is not ideal for scripting / simple usage and inspection by developer.

Objectives:

~~- [ ] Create a simple to use whl installation for developers / consumers of kmir~~
~~- [ ] Slim the docker image as an easy CI callable for kmir in CI~~

Deploy Docker image
Simple WF script demonstrate testing execution using kmir posted docker image

MVP

CI Run executing single test using published docker image to dockerhub

The previous code was creating a new proof object from the spec file (first claim). Instead, the proof needs to be loaded from a file in the proof directory. Note that `APRProver.read_proof` and `APRProver/read_proof_data` have different expectations to how the proof is stored. The latter method has to be used.

Creating README.

Adding section for unsafe arithmetics

Jost corrected an error with `isize` and `usize`. And I changed some of the copy in the README. Also updates the branch to current master --------- Co-authored-by: Jost Berthold <jost.berthold@gmail.com> Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>

Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Jost Berthold <jost.berthold@gmail.com>

Reverts #512 --------- Co-authored-by: devops <devops@runtimeverification.com>

Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Jost Berthold <jost.berthold@gmail.com>

… bugs and challenge to fully isolate built dependencies into the src contained for packaging and installation deployiment. Current problem: - Post installation of whl .cache/kdist-<hash> file is not available and hardcoded to look in ~/.cache/kdist-<hash> - This needs a generalized location or be installed to site-package swith the rest of the library files for python packaging to work as intended. - Unresolved understanding of where stable-mir-json artifacts need to be stored / referenced for kmir prove - Published a single docker image from manual built image to produce an alias poetry-kmir usable image within CI, but is not ideal for scripting / simple usage and inspection by developer.

.github/workflows/release.yml

.github/workflows/test.yml

- Updating image tag to drop k_release from tag modified: .github/workflows/test.yml - Droping k_release from tag.

- Modify the WF to drop mdofying internal container user, rely on internal user and user id set by container manager. - docker cp copies file to the container with the internal user target uid to match internal container env, don't overwork this. - Maintain exec commands to use -l to consume internal user env modified: Dockerfile.kmir

…s move it up incase anyone using our contaienr is the first user on their own system

…uid to define our container ids try not loading bash profile

…ive to host

F-WRunTime · 2025-04-08T05:59:10Z

@jberthold Sorry for delay, I needed to step away this was stumping me.
I've got something working and it works both locally and in CI.
Local execution is a bit easier as the file directories are created by pyk as expected in the shared volume but GH runners it was not as simple, and a bit of a challenge.

jberthold · 2025-04-08T06:27:53Z

@jberthold Sorry for delay, I needed to step away this was stumping me. I've got something working and it works both locally and in CI. Local execution is a bit easier as the file directories are created by pyk as expected in the shared volume but GH runners it was not as simple, and a bit of a challenge.

No problem at all. I was just going to try this one thing on a whim... but you got it building green already! 🎉
Another thing I did today was to run fixuid without -q, and found there are a lot of small files that take time to chown on startup, which we can just delete. Just testing it once more, then I can add that to the dockerfile.

jberthold · 2025-04-08T06:37:59Z

@jberthold Sorry for delay, I needed to step away this was stumping me. I've got something working and it works both locally and in CI. Local execution is a bit easier as the file directories are created by pyk as expected in the shared volume but GH runners it was not as simple, and a bit of a challenge.

No problem at all. I was just going to try this one thing on a whim... but you got it building green already! 🎉 Another thing I did today was to run fixuid without -q, and found there are a lot of small files that take time to chown on startup, which we can just delete. Just testing it once more, then I can add that to the dockerfile.

I think maybe we merge this PR and I make another one with my changes to the Dockerfile, so we get this to master sooner.

jberthold

Let's merge this PR and iterate.
I would still like to modify the test so it will use fixuid but anyway there are more changes to the Dockerfile waiting, I'll do it on the next PR

jberthold and others added 24 commits March 12, 2025 15:45

Add files and description for an example program/proof

30d4610

make proof-dir required for kmir prove view command

d4ea348

Use usize in source code for consistency

9082e00

Adding unchecked specs

f992c9d

Fixing requires clause for unchecked operations

0ef0094

Adding rust-verification-proofs folder

fc99d92

Removing scratch

1819def

Update README.md

5f4ffeb

Creating README.

Update README.md

7a546e9

Adding section for unsafe arithmetics

Removing repo from command

592b276

FIx wording

570a63e

Update README.md

d421709

Fix operation names and requires condition

e2de329

Update README.md

b7fe354

Merge branch 'master' into sample-challenge-11-proofs

6f612ca

Merging master into branch (#512)

9aa7975

Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Jost Berthold <jost.berthold@gmail.com>

Revert "Merging master into branch" (#513)

74a18a1

Reverts #512 --------- Co-authored-by: devops <devops@runtimeverification.com>

Manually resolving conflict with master

e1ba203

Merging master into branch (#514)

d557313

Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Jost Berthold <jost.berthold@gmail.com>

adapt spec files to updated master

293735d

format and adjust json files, adjust README

f109657

F-WRunTime requested review from ACassimiro, gtrepta and jberthold March 28, 2025 22:30

rv-auditor and others added 2 commits March 28, 2025 22:31

Set Version: 0.3.110

80e792f

Remove unfinished thought

e772ece

F-WRunTime changed the title ~~Adding First round of attempt to package kmir to python whl + Docker image~~ Adding First round of attempt to package kmir to python whl + Publish Docker image Mar 29, 2025

F-WRunTime requested review from dkcumming and removed request for ACassimiro April 2, 2025 21:46

- Drop docker cp and just mount the folder to the cp drop location

d0a559f

jberthold approved these changes Apr 2, 2025

View reviewed changes

.github/workflows/release.yml Outdated Show resolved Hide resolved

.github/workflows/test.yml Outdated Show resolved Hide resolved

.github/workflows/test.yml Outdated Show resolved Hide resolved

F-WRunTime and others added 19 commits April 2, 2025 16:22

modified: .github/workflows/release.yml

f9beb10

- Updating image tag to drop k_release from tag modified: .github/workflows/test.yml - Droping k_release from tag.

Moving workspace in running container to 'workspace' from '/home/kmir'

adc6b0a

Do we need to create folders before they are written to?

50753da

Revert some testing, and remove 'docker cp'

7b891c4

Revert removal of fixuid

4832103

Workdir set for exec commands

ab89627

The UID used is generally for the very first created on a system. Let…

e3691da

…s move it up incase anyone using our contaienr is the first user on their own system

Set Version: 0.3.113

963931c

Merge branch 'master' into challenge-11-ci

731656c

Set Version: 0.3.113

a291250

Merge branch 'master' into challenge-11-ci

60b4ab5

Set Version: 0.3.114

1ba1eff

EXPERIMENT set UID:GID in docker exec during test

32b9806

reworking test execution setup with minor tweaks since we rely on fix…

bbd4e1b

…uid to define our container ids try not loading bash profile

Remove IDs, drop extra flags, add interative/tty to exec.

3b858b2

try and see the output of the test to see hwat failed

88b881e

Lets do some debug

c992ef6

Rework proof folder generation workaround container permissions relat…

be18c88

…ive to host

F-WRunTime requested a review from jberthold April 8, 2025 05:57

jberthold approved these changes Apr 8, 2025

View reviewed changes

F-WRunTime merged commit f2c9a09 into master Apr 8, 2025
6 checks passed

F-WRunTime deleted the challenge-11-ci branch April 8, 2025 06:43

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Publish Docker image + Example CI WF + Upload to dockerhub#516

Publish Docker image + Example CI WF + Upload to dockerhub#516
F-WRunTime merged 89 commits intomasterfrom
challenge-11-ci

F-WRunTime commented Mar 28, 2025 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

F-WRunTime commented Apr 8, 2025

Uh oh!

jberthold commented Apr 8, 2025

Uh oh!

jberthold commented Apr 8, 2025

Uh oh!

jberthold left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

F-WRunTime commented Mar 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Objectives:

MVP

Uh oh!

Uh oh!

Uh oh!

Uh oh!

F-WRunTime commented Apr 8, 2025

Uh oh!

jberthold commented Apr 8, 2025

Uh oh!

jberthold commented Apr 8, 2025

Uh oh!

jberthold left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

F-WRunTime commented Mar 28, 2025 •

edited

Loading