Skip to content

Conversation

@schaafjs
Copy link
Contributor

  1. Adds missing includes (lib/label lib/communication) in the Makefile to DY_INCLUDE_DIRS.
  2. As for_allP is now part of F* itself, the containing module also needs to be imported (from FStar.List.Tot.Base) in all the places where it is used:
    • DY.NSLP.Invariants.fst
    • DY.OnlineA.Invariants.fst
    • DY.OnlineS.Invariants.fst

@TWal
Copy link
Contributor

TWal commented Jun 13, 2025

Looks like although GitHub allows me to change your branch via the website (to merge the branch main), I cannot do that on the command line with git?

Right now the CI will fail because you need to update the file flake.lock which pins the dependencies of this repository. I have done that for you on the shaafjs branch, you just have to merge it (or alternatively, commit the flake.lock present there)

@schaafjs
Copy link
Contributor Author

I couldn't figure the merging out and have updated the lock file directly instead.

Copy link
Contributor

@TWal TWal left a comment

Choose a reason for hiding this comment

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

Looks good to me, thanks!

I will let @qaphla or @fabian-hk review and merge since I didn't write any code in this repo.

@qaphla qaphla merged commit cef2764 into REPROSEC:main Jun 13, 2025
1 check passed
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.

3 participants