Skip to content

Avoid java compilation error when user code defines Get in a codatatype #11150

Avoid java compilation error when user code defines Get in a codatatype

Avoid java compilation error when user code defines Get in a codatatype #11150

Triggered via pull request January 17, 2025 16:20
Status Failure
Total duration 18s
Artifacts

doc-tests.yml

on: pull_request
check-deep-tests  /  check-deep-tests
5s
check-deep-tests / check-deep-tests
doctests
0s
doctests
Fit to window
Zoom out
Zoom in

Annotations

1 error
check-deep-tests / check-deep-tests
Last run of nightly-build.yml did not succeed: https://github.com/dafny-lang/dafny/actions/runs/12831090540 At the time of checking, no fix was underway. - Please first check https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml . If you see any queued or in progress run on nightly-build.yml, just re-run this test once it is finished.- If not, and you are a Dafny developer, please fix the issue by creating a PR with the label [run-deep-tests], have it reviewed and merged, and then trigger the workflow on nightly-build.yml with the URL https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml . With such a label, you can merge a PR even if tests are not successful, but make sure the deeps one are! If you do not have any clue on how to fix it, at worst you can revert all PRs from the last successful run and indicate the authors they need to re-file their PRs and add the label [run-deep-tests] to their PRs