File tree 2 files changed +12
-2
lines changed
2 files changed +12
-2
lines changed Original file line number Diff line number Diff line change @@ -124,6 +124,7 @@ config.oneshot.json: config.json
124
124
jq ' .extraModules += ["Oneshot"]' < config.json > config.oneshot.json
125
125
126
126
Outputs/src/oneshot/Oneshot/Main.lean : Oneshot/lean3-in/main.ast.json Oneshot/lean4-in/build/lib/Oneshot.trace config.oneshot.json
127
+ mkdir -p Logs/
127
128
./build/bin/mathport config.oneshot.json Oneshot::main >> Logs/oneshot.out 2> >( tee -a Logs/oneshot.err >&2 )
128
129
129
130
oneshot : Outputs/src/oneshot/Oneshot/Main.lean
Original file line number Diff line number Diff line change 2
2
# Script to download artifacts from a release.
3
3
# Usage: `./download-release.sh nightly-2021-11-30`
4
4
5
- RELEASE=$1 # e.g. nightly-2021-11-30
5
+ if [ -z ${1+x} ]; then
6
+ RELEASE=`
7
+ curl -H " Accept: application/vnd.github+json" -H " X-GitHub-Api-Version: 2022-11-28" \
8
+ https://api.github.com/repos/leanprover-community/mathport/releases \
9
+ | jq ' last([.[].tag_name | select(startswith("nightly-"))] | sort | .[])' -r
10
+ `
11
+ else
12
+ RELEASE=$1 # e.g. nightly-2021-11-30
13
+ fi
14
+ echo " getting release $RELEASE "
6
15
7
16
if [ -z " $RELEASE " ]; then
8
- echo " Usage: ./download-release.sh nightly-YYYY-MM-DD"
17
+ echo " Usage: ./download-release.sh [ nightly-YYYY-MM-DD] "
9
18
echo " See https://github.com/leanprover-community/mathport/releases for available releases"
10
19
exit 1
11
20
fi
You can’t perform that action at this time.
0 commit comments