Easily test lean4 patch

Stream: lean4

[cognivore]

Dear all,

I'm making some patches to lean4, which I would like to test against existing codebases by swapping out lean-toolchain with a reference to a github release, or, better yet, commit hash in a fork. How would I go about it?

It seems to be attempting to download from a very peculiar place: https://github.com/cognivore/lean4/releases/expanded_assets/alt-backend.

Finally, I don't quite understand if I need to provide it with binary releases or is it possible to have lake call elan to compile lean somehow. Sorry for silly questions, I'll read the code of the corresponding tools, but perhaps someone knows off the bat how to develop in a fork.

[Notification Bot]

cognivore has marked this topic as unresolved.

[cognivore]

Alright, things still don't work.

I made a release of some branch, which caused some job to run successfully https://github.com/cognivore/lean4/actions/runs/3754045206

However, when I go to releases section in the repository and find the release made for this branch, I don't see any files generated: https://github.com/cognivore/lean4/releases/tag/carboncopy-1-2-1

The rights of the workflows are set to R+W (see screenshot):

image.png

[Gabriel Ebner]

Hmm, it only ran the "Nix CI" workflow but not the "CI" workflow. The "CI" workflow is the one which uploads the releases.

[Scott Morrison]

(Necromancing a thread to note that I had the same problem, but found after clicking the "Actions" tab in github, then selecting "CI" on the left pane, that github had disabled the workflow due to inactivity. Re-enabling the workflow, and then force pushing the tag again, seems to have started the workflow correctly.)