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.

Sign up for GitHub

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

Jump to bottom

feat(ci): add Lean testing in the CI #871

Merged
merged 5 commits into from
Jan 30, 2025
Merged

feat(ci): add Lean testing in the CI #871

merged 5 commits into from
Jan 30, 2025
+30 −4

Conversation

RaitoBezarius
Copy link
Contributor

@RaitoBezarius RaitoBezarius commented Jan 13, 2025 •
edited
Loading

This ensures that all changes to the Lean backend are tested by recompiling the Lean files with Lean itself via the coverage CI entrypoint.

I'm not exactly sure if you are fine with the solution to install Lean, I have other options:

  • Bring Nix and install elan via Nix and use the Nix store caching mechanism
  • Remove caching for elan
  • Your preferred solution

Let me know what you prefer and I will adapt this PR. Additionally, I have a Nix scaffolding setup (default/shell) which is quite popular for people working on that environment, if you are interested into me contributing it, please let me know. I can also take maintenance ownership on that if needed, obviously.

cc @javra

Signed-off-by: Raito Bezarius [email protected]

@RaitoBezarius
Copy link
Contributor Author

I noticed that Lean tests are actually already covered by the test coverage job, I will remove the extension of the core tests and change this to build the emitted Lean project.

@RaitoBezarius
Copy link
Contributor Author

@javra This is ready now, I think.

@RaitoBezarius RaitoBezarius force-pushed the lean-ci branch 3 times, most recently from 5f294bb to e7e5674 Compare January 16, 2025 14:04
@bacam
Copy link
Contributor

bacam commented Jan 16, 2025

Maybe bash -s -- -y?

@bacam
Copy link
Contributor

bacam commented Jan 16, 2025

bash will treat -y as its own option if there's no --.

@RaitoBezarius
Copy link
Contributor Author

bash will treat -y as its own option if there's no --.

I was not sure that bash had -- processing, but yeah, I think this should do the job.

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 16, 2025 •
edited
Loading

Test Results

   12 files  ±0     24 suites  ±0   0s ⏱️ ±0s
  759 tests ±0    759 ✅ ±0  0 💤 ±0  0 ❌ ±0 
2 503 runs  ±0  2 503 ✅ ±0  0 💤 ±0  0 ❌ ±0 

Results for commit 555d647. ± Comparison against base commit 4db7000.

♻️ This comment has been updated with latest results.

@javra
Copy link
Collaborator

javra commented Jan 16, 2025

Besides lake not being found: We'd also need to run the build such that warnings are ignored (because we're using sorry liberally)

Alasdair
Alasdair reviewed Jan 16, 2025
View reviewed changes
.github/workflows/coverage.yml Outdated
uses: actions/cache/restore@v3
with:
path: ~/.elan
key: ${{ matrix.os }}-${{ matrix.version }}-cov
Copy link
Collaborator

Choose a reason for hiding this comment

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

Can we use the same key here as our opam cache, or will they end up clobbering each other?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I think they are going to clobber each other actually.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

(so I would prefix the key by elan-)

@RaitoBezarius
Copy link
Contributor Author

Besides lake not being found: We'd also need to run the build such that warnings are ignored (because we're using sorry liberally)

During my local tests, warnings does not cause nonzero exit status and does not make the pipeline fail. But yeah.

@RaitoBezarius
Copy link
Contributor Author

@bacam could I bother you to kick again a CI run?

@jprider63
Copy link
Collaborator

@Alasdair taking over this for now.

@Alasdair
Copy link
Collaborator

CI is now running lake, but I get some errors. Is this just because this branch is behind?

Failed: lake --dir enum/out build
stdout:
✔ [2/4] Built Out.Sail.Sail
✖ [3/4] Building Out
trace: .> LEAN_PATH=enum/out/./.lake/build/lib LD_LIBRARY_PATH= /home/runner/.elan/toolchains/stable/bin/lean enum/out/./././Out.lean -R enum/out/././. -o enum/out/./.lake/build/lib/Out.olean -i enum/out/./.lake/build/lib/Out.ilean -c enum/out/./.lake/build/ir/Out.c --json
error: enum/out/./././Out.lean:9:18: function expected at
  SailM
term has type
  ?m.132
error: Lean exited with code 1
Some required builds logged failures:
- Out

@RaitoBezarius
Copy link
Contributor Author

Off the top of my head, I was able to lake build things myself locally so it's surprising to see errors, could be Lean version.

@tobiasgrosser
Copy link
Collaborator

We should just merge the latest sail2 branch and see where things are standing then.

@tobiasgrosser
Copy link
Collaborator

Also, this PR fixes some lean bugs: #920.

@tobiasgrosser
Copy link
Collaborator

This still fails with:

trace: .> LEAN_PATH=match/out/./.lake/build/lib LD_LIBRARY_PATH= /home/runner/.elan/toolchains/stable/bin/lean match/out/./././Out.lean -R match/out/././. -o match/out/./.lake/build/lib/Out.olean -i match/out/./.lake/build/lib/Out.ilean -c match/out/./.lake/build/ir/Out.c --json
error: match/out/./././Out.lean:9:18: function expected at
  SailM
term has type
  ?m.132
error: Lean exited with code 1
Some required builds logged failures:
- Out

@javra
Copy link
Collaborator

javra commented Jan 29, 2025

Well it's not been rebased yet, has it?

@tobiasgrosser
Copy link
Collaborator

Not on #920 yet.

@javra
Copy link
Collaborator

javra commented Jan 29, 2025

#920 doesn't fix the error message that you posted, but some stuff in between might have

@RaitoBezarius @Alasdair
fix(test/lean/run_tests): ensure the directory exist, do not fail wit…
192e919 
…h EEXIST

If the directory already exist, it's fine, no need to fail with EEXIST.

This fixes the situation where the bug already exist.

Signed-off-by: Raito Bezarius <[email protected]>
@RaitoBezarius @Alasdair
fix(sail): POSIX compliance for shebang script
81aa893 
/bin/bash is not guaranteed to exist on all Linux distributions, NixOS
does not have one.

Prefer `/usr/bin/env` which should really (empirically) always exist.

Signed-off-by: Raito Bezarius <[email protected]>
RaitoBezarius and others added 3 commits January 29, 2025 21:49
@RaitoBezarius @Alasdair
chore(lean/run_tests): ensure the basename directories are cleaned up
51bf358 
Restovers can remains due to spurious failures as we are not catching
exceptions in the middle that may prevent the final `rm` to run.

If we are not doing that, the next run will cause EEXIST errors.

Signed-off-by: Raito Bezarius <[email protected]>
@RaitoBezarius @Alasdair
feat(lean/run_tests): Test generated Lean code using Lean itself
44f9ff3 
This reuses the various lean-toolchain information and download an
ad-hoc Lean version based on this.

Signed-off-by: Raito Bezarius <[email protected]>
@Alasdair
CI: Update elan cache and path
555d647
@Alasdair
Copy link
Collaborator

Looks like that commit reduced the number of errors from 6 down to 4. I can make it ignore those tests and then we can merge. Whichever commit fixes each test can then just remove them from the ignore list.

@tobiasgrosser
Copy link
Collaborator

Sounds great. Thank you.

@javra
Copy link
Collaborator

javra commented Jan 30, 2025

The only issue seems to be that the SailM definition should be present whenever there's a monadic function, not only when there's registers. I'll have a look. /cc @lfrenot

@javra
Copy link
Collaborator

javra commented Jan 30, 2025

I'm on it, fix incoming

@javra
Copy link
Collaborator

javra commented Jan 30, 2025

#922 should fix it

@javra
Copy link
Collaborator

javra commented Jan 30, 2025

(Openened a PR to make the empty type hashable to have a more homogeneous solution later)

@javra javra mentioned this pull request Jan 30, 2025
Merged
@bacam bacam closed this in #922 Jan 30, 2025
@bacam
Copy link
Contributor

bacam commented Jan 30, 2025 •
edited
Loading

Ahem, #922 did not fix it in that sense...

@bacam bacam reopened this Jan 30, 2025
@bacam bacam merged commit e7f1262 into rems-project:sail2 Jan 30, 2025
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Alasdair Alasdair Alasdair left review comments

Assignees

@Alasdair Alasdair

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@RaitoBezarius @bacam @javra @jprider63 @Alasdair @tobiasgrosser