Rv kmir milestone 4

[ehildenb]

Milestone Delivery Checklist

• The milestone-delivery-template.md has been copied and updated.
• This pull request is being made by the same account as the accepted application.
• I have disclosed any and all sources of reused code in the submitted repositories and have done my due diligence to meet its license requirements.
• In case of acceptance, an invoice must be submitted and the payment will be transferred to the Polkadot/fiat account provided in the application.
• The delivery is according to the Guidelines for Milestone Deliverables.

Link to the application pull request: w3f/Grants-Program#1422 < please fill this in with the PR number of your application.

[takahser]

@ehildenb could you please remove the changes made to the workflows? Please note that the delivery should only include a single delivery file (which you included) but nothing else.

[takahser]

@ehildenb On top of the comments made earlier, I had some issues when running your code. You can find my evaluation here. LMK if you have any questions.

[takahser]

Suggested change

	| **0d.** | Docker | [Dockerfile](https://github.com/runtimeverification/mir-semantics/blob/milestone4-deliverable/Dockerfile |
	| **0d.** | Docker | [Dockerfile](https://github.com/runtimeverification/mir-semantics/blob/milestone4-deliverable/Dockerfile] |

[dkcumming]

I think this was meant to be )

[dkcumming]

Hi @takahser, sorry I didn't get any notifications when this PR was created. I can help you out with the evaluation.

Docker test run problems

This is strange to me, because our test runner for CI is the same docker script (link1, link2) and has no problem, and I ran the docker same commands locally on my machine just now to check and they executed as expected. Could you provide some details for the system you are running these on?

Documentation

We are in the process of updating the documentation currently. We can add this into the PR, I have made an issue here.

[dkcumming]

In case it helps I will link some key PR's related to the kup nix infrastructure:

• kmir 194
• kmir 199
• kup 72

[takahser]

@dkcumming

Could you provide some details for the system you are running these on?

I'm using a macbook pro m2, running macOS 14.1.1
What machine and OS are you using?

We are in the process of updating the documentation currently. We can add this into the PR, I have made an runtimeverification/mir-semantics#271.

Thanks, I've updated the evaluation.

Also, please have a look at the inline comments as well.

[dkcumming]

Hi @takahser, just giving you an update. I am running the tests on Ubuntu 22.04.3 LTS. Last week I had some discussion with a colleague that also has an M2 macbook, and after some time he was able to reproduce the error that you have. He did not have a minimised reproducer yet, but believes it is related to docker login on the machine. I will continue with him to figure out what the exact problem is.

[dkcumming]

@takahser So we have spent a bit of time trying to determine the root of the problem that you experienced, and it appears that there are some behaviours with Docker on Mac Silicon machines that create this issue. We have discussed it at length, and have decided that we will not explicitly support running the test suite through docker directly on Mac Silicon. This does not mean that the tests cannot be run on Mac Silicon however, it just means that the Nix test runner should be used (part of this delivery actually). A PR has been made that explicitly includes Mac Silicon as part of CI to demonstrate that it is supported.

The wording of the delivery indicates that docker is intended to be used for CI, and so we feel that all of this is in line with the delivery. If a different machine (not Mac Silicon) is available for you to use then the Docker commands run should work (all of our testing has worked on other machines so far). Happy to discuss anything in more detail if necessary of course.

[takahser]

@dkcumming okay, I'm going to re-test it on a ubuntu AWS instance in that case. Will keep you posted, thanks!

[takahser]

@ehildenb I've tested on ubuntu, now the tests pass when using docker. However, I wasn't able to build the project using make build:

# make build
make: *** No rule to make target 'build'.  Stop.

Any idea what could be the issue here?

Update:

I'm not sure if I ran it in the wrong directory, but even when running it in the mir-semantics directory, it fails:

~/mir-semantics/kmir# make build
poetry install

  RuntimeError

  The Poetry configuration is invalid:
    - Additional properties are not allowed ('group' was unexpected)
  

  at /usr/lib/python3/dist-packages/poetry/core/factory.py:43 in create_poetry
       39│             message = ""
       40│             for error in check_result["errors"]:
       41│                 message += "  - {}\n".format(error)
       42│ 
    →  43│             raise RuntimeError("The Poetry configuration is invalid:\n" + message)
       44│ 
       45│         # Load package
       46│         name = local_config["name"]
       47│         version = local_config["version"]
make: *** [Makefile:30: poetry-install] Error 1

[dkcumming]

@takahser Hi, I will help out with this one.

Running the commands for poetry means that you must be in the directory of pyproject.toml (or manually direct poetry to that location). This was implied (poorly) by the line for building being located in the README in the kmir directory. We realised that the split of two README files was confusing and have consolidated the information into one, which now directs the user to navigate to the kmir directory first.
EDIT: I just realised that you were running make build not poetry install, I had my wires crossed there. make commands interact with a Makefile which is located in kmir directory. By the same reasoning as what I described above, you need to run the command in the same directory as the file (or manually point to it).

As for the error. First glance is that there is a permissions issue. I can investigate further, but I would like to know the set up you are running this on. Could you provide any details for that? Also could you please run ls -l from the kmir directory and post that? I want to confirm that the permissions are the same.

[takahser]

@dkcumming sure no problem:

~/mir-semantics/kmir# ls -l
total 80
-rwxrwxr-x 1 root root  6141 Dec 13 03:50 Makefile
-rwxrwxr-x 1 root root   560 Dec 13 03:50 check_k_version.sh
-rwxrwxr-x 1 root root  2460 Dec 13 03:50 doit.sh
-rwxrwxr-x 1 root root  3975 Dec 13 03:50 flake.lock
drwxrwxr-x 2 root root  4096 Dec 13 03:50 k-src
-rwxrwxr-x 1 root root   417 Dec 13 03:50 kbuild.toml
-rwxrwxr-x 1 root root 38036 Dec 13 03:50 poetry.lock
-rwxrwxr-x 1 root root  1080 Dec 13 03:50 pyproject.toml
-rwxrwxr-x 1 root root   185 Dec 13 03:50 set_env.sh
drwxrwxr-x 4 root root  4096 Dec 13 03:50 src

I can investigate further, but I would like to know the set up you are running this on.

I'm running it on a EC2 AWS instance that runs on ubuntu 22:

# lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 22.04.3 LTS
Release:        22.04
Codename:       jammy

[takahser]

@ehildenb as discussed in today's call, @semuelle will take a look at it next, since we weren't able to resolve the poetry issues on AWS when building the code.

[dkcumming]

@takahser and @semuelle, all good. Just letting you know it was me on the call with you, and I will be the best point of contact. @semuelle, let me know if I can help with anything

[takahser]

@dkcumming right, thanks for pointing out! 👍

[ehildenb]

@takahser and @semuelle this milestone review is taking quite some time now. We are testing the semantics in a CI environment continuously, and have provided instructions and utilities to make it easier to install via kup utility, let us know if there are other specific guidances we can provide on the building and installation of the tool. Providing instructions on how to manage Nix or Docker seems outside the scope of this tool though, as there are comprehensive guides to those elsewhere.

Let us know, we would like to move this along so we can focus on next steps with the semantics!

[semuelle]

Hi @dkcumming. As @takahser mentioned, I took over the evaluation. Good news, I don't have a Mac and everything worked basically out of the box. The only thing that's missing is D2, the article. You can add it to the delivery document or share it privately by email.

[dkcumming]

@semuelle great news. Here is the article published on our website, we previously worked in coordination with @takahser for the publishing of this article.

[semuelle]

Thanks, @dkcumming. Your milestone is hereby accepted. You can find the evaluation notes here.

Congratulations on completing the grant, and best of luck going forward! Hope to see you around.

[github-actions]

🪙 Please fill out the invoice form in order to initiate the payment process. Thank you!

[github-actions]

We noticed that this is the last milestone of your project. Congratulations on completing your grant! 🎊

So, where to from here? First of all, you should join our Grants Community chat, if you haven't already, so we can stay in touch.
If you are looking for continuative support for your project, there are quite a few options. The main goal of the W3F grants program is to support research as well as early-stage technical projects. If your project still falls under one of those categories, you might want to apply for a follow-up grant. However, depending on your goals and project status, there are other support programs in our ecosystem that might be better suited as the next step. For example, projects with a Business Case/Token should look into the Substrate Builders Program or VC Funding and Common Good projects have a good chance of receiving Treasury Funding. If you are looking for guidance, the team at https://substrate.io/ecosystem/square-one/ has compiled a list of ecosystem support sources and are happy to help you navigate it.

For a more comprehensive list, see our Alternative Funding page. Let us know if you have any questions regarding the above. We are more than happy to point you to additional resources and help you determine the best course of action.
Lastly, we hope your W3F grant was a success and we want to thank you for being part of the journey!

[dkcumming]

@takahser @semuelle Thank you very much. It was a pleasure to work with you!

[ehildenb]

I've submitted the invoice form.