File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 4040 ~/.elan/bin/lake exe LeanCopilot/download
4141 - name : Build tests
4242 run : ~/.elan/bin/lake build LeanCopilotTests
43-
44- build-beta :
45- runs-on : windows-latest
46- name : BuildBeta
47- continue-on-error : true
48- steps :
49- - name : Checkout project
50- uses : actions/checkout@v5
51- with :
52- fetch-depth : 0
53- - name : Install Git LFS
54- run : |
55- git lfs update --force
56- git lfs install
57- - name : Set up elan
58- run : curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
59- - name : Add .lake/build/lib to PATH
60- shell : bash
61- run : |
62- echo "$GITHUB_WORKSPACE/.lake/build/lib" >> $GITHUB_PATH
63- - name : Build project
64- run : ~/.elan/bin/lake build
65- - name : Download model
66- run : |
67- ~/.elan/bin/lake exe LeanCopilot/download
68- - name : Build tests
69- run : ~/.elan/bin/lake build LeanCopilotTests
You can’t perform that action at this time.
0 commit comments