Skip to content

Commit 7554f5a

Browse files
gallaisgallais
committed
Merge branch 'master' into experimental
2 parents eedf046 + 1198e33 commit 7554f5a

File tree

199 files changed

+6565
-3264
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

199 files changed

+6565
-3264
lines changed

‎.gitignore

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
.*.swp
55
*.agdai
66
*.agda.el
7+
./_build/*
78
.DS_Store
89
*.lagda.el
910
*.hi
@@ -17,3 +18,5 @@ EverythingSafe.agda
1718
EverythingSafeGuardedness.agda
1819
EverythingSafeSizedTypes.agda
1920
html
21+
Haskell
22+
MAlonzo

‎.travis.yml

Lines changed: 174 additions & 143 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,6 @@ branches:
66

77
dist: xenial
88

9-
cache:
10-
directories:
11-
- $HOME/.cabsnap
12-
139
matrix:
1410
include:
1511
- env:
@@ -25,142 +21,177 @@ matrix:
2521
sources:
2622
- hvr-ghc
2723

28-
before_install:
29-
- export PATH=/opt/ghc/$GHC_VER/bin:/opt/cabal/$CABAL_VER/bin:/opt/alex/$ALEX_VER/bin:/opt/happy/$HAPPY_VER/bin:~/.cabal/bin/:$PATH;
30-
31-
install:
32-
- cabal update
33-
- sed -i 's/^jobs:/-- jobs:/' $HOME/.cabal/config
34-
35-
# installing dependencies
36-
- cabal install alex-$ALEX_VER happy-$HAPPY_VER cpphs
37-
38-
# installing Agda
39-
# Even if there seems to be duplicated code for master & experimental,
40-
# DO NOT refactor: they regularly get out of sync (typically master
41-
# builds with the released version while experimental uses some dev
42-
# version).
43-
44-
# No matter the path, we should generate a $HOME/installplan.txt to
45-
# check whether the cache needs updating.
46-
47-
- if [[ $TRAVIS_BRANCH = "master" ]]; then
48-
cd ../ &&
49-
git clone https://github.com/agda/agda &&
50-
cd agda &&
51-
git checkout 08dd23df8dd894737af98463f0b3f69d616e7b48 &&
52-
cabal install --only-dependencies --dry -v > $HOME/installplan.txt ;
53-
fi
54-
55-
- if [[ $TRAVIS_BRANCH = "experimental" ]]; then
56-
cd ../ &&
57-
git clone https://github.com/agda/agda &&
58-
cd agda &&
59-
git checkout c2d5ec4b2403c68d615b81258d6131774e492797 &&
60-
cabal install --only-dependencies --dry -v > $HOME/installplan.txt ;
61-
fi
62-
63-
# checking whether .ghc is still valid
64-
- sed -i -e '1,/^Resolving /d' $HOME/installplan.txt; cat $HOME/installplan.txt
65-
- touch $HOME/.cabsnap/installplan.txt
66-
- mkdir -p $HOME/.cabsnap/ghc $HOME/.cabsnap/lib $HOME/.cabsnap/share $HOME/.cabsnap/bin
67-
- if diff -u $HOME/.cabsnap/installplan.txt $HOME/installplan.txt;
68-
then
69-
echo "cabal build-cache HIT";
70-
rm -rfv .ghc;
71-
cp -a $HOME/.cabsnap/ghc $HOME/.ghc;
72-
cp -a $HOME/.cabsnap/lib $HOME/.cabsnap/share $HOME/.cabsnap/bin $HOME/.cabal/;
73-
else
74-
echo "cabal build-cache MISS";
75-
rm -rf $HOME/.cabsnap;
76-
mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;
77-
fi
78-
79-
- if [[ $TRAVIS_BRANCH = "master" ]]; then
80-
cabal install ;
81-
fi
82-
83-
- if [[ $TRAVIS_BRANCH = "experimental" ]]; then
84-
cabal install ;
85-
fi
86-
87-
# snapshot package-db on cache miss
88-
- echo "snapshotting package-db to build-cache";
89-
mkdir $HOME/.cabsnap;
90-
cp -a $HOME/.ghc $HOME/.cabsnap/ghc;
91-
cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin $HOME/installplan.txt $HOME/.cabsnap/;
92-
93-
- if [[ $TRAVIS_BRANCH = "master" ]]; then
94-
cd ../ ;
95-
fi
96-
97-
- if [[ $TRAVIS_BRANCH = "experimental" ]]; then
98-
cd ../ ;
99-
fi
100-
101-
# installing fix-whitespace
102-
- git clone https://github.com/agda/fix-whitespace --depth=1
103-
- cd fix-whitespace
104-
- cabal install fix-whitespace.cabal
105-
- cd ../
106-
107-
# generating Everything.agda
108-
- cd agda-stdlib
109-
- cabal install lib.cabal
110-
- runghc GenerateEverything.hs
111-
112-
# setting up travis-specific scripts and files
113-
- cp travis/* .
114-
115-
before_script:
116-
- export RTS_OPTIONS="+RTS -M3.5G -H3.5G -A128M -RTS"
117-
118-
script:
119-
# generating index.agda
120-
- ./index.sh
121-
# detecting whitespace violations
122-
- fix-whitespace --check
123-
# expose the value of RTS_OPTIONS
124-
- echo $RTS_OPTIONS
125-
# checking safe modules build with --safe
126-
- agda $RTS_OPTIONS -i . -i src/ --safe EverythingSafeGuardedness.agda
127-
- agda $RTS_OPTIONS -i . -i src/ --safe EverythingSafeSizedTypes.agda
128-
# detecting basic compilation errors
129-
- agda $RTS_OPTIONS -i . -i src/ -c --no-main Everything.agda
130-
# compiling & running the examples using the FFI
131-
- agda $RTS_OPTIONS -i . -i src/ -c README/Foreign/Haskell.agda && ./Haskell
132-
# building the docs
133-
- agda $RTS_OPTIONS -i . -i src/ --html safe.agda
134-
- agda $RTS_OPTIONS -i . -i src/ --html index.agda
135-
136-
# moving everything to the appropriate directory
137-
- if [[ $TRAVIS_BRANCH = "master" ]]; then
138-
mv html/* . ;
139-
fi
140-
- if [[ $TRAVIS_BRANCH = "experimental" ]]; then
141-
mkdir -p experimental/ ;
142-
mv html/* experimental/ ;
143-
fi
144-
145-
after_success:
146-
# uploading to gh-pages
147-
- git init
148-
- git config --global user.name "Travis CI bot"
149-
- git config --global user.email "[email protected]"
150-
- git remote add upstream https://[email protected]/agda/agda-stdlib.git &>/dev/null
151-
- git fetch upstream && git reset upstream/gh-pages
152-
- if [[ $TRAVIS_BRANCH = "master" ]]; then
153-
git checkout HEAD -- v0.16/ v0.17/ v1.0/ v1.1/ v1.2/ experimental/ ;
154-
fi
155-
- if [[ $TRAVIS_BRANCH = "experimental" ]]; then
156-
git checkout HEAD -- *.html v0.16/ v0.17/ v1.0/ v1.1/ v1.2/ ;
157-
fi
158-
- git add -f \*.html
159-
- git commit -m "Automatic HTML update via Travis"
160-
- if [[ $TRAVIS_PULL_REQUEST = "false" && ($TRAVIS_BRANCH = "master" || $TRAVIS_BRANCH = "experimental") ]]; then
161-
git push -q upstream HEAD:gh-pages &>/dev/null;
162-
fi
163-
164-
notifications:
165-
email: false
166-
24+
cache:
25+
directories:
26+
- $HOME/.cabsnap
27+
28+
before_install:
29+
- export PATH=/opt/ghc/$GHC_VER/bin:/opt/cabal/$CABAL_VER/bin:/opt/alex/$ALEX_VER/bin:/opt/happy/$HAPPY_VER/bin:~/.cabal/bin/:$PATH;
30+
31+
install:
32+
- cabal update
33+
- sed -i 's/^jobs:/-- jobs:/' $HOME/.cabal/config
34+
35+
# installing dependencies
36+
- cabal install alex-$ALEX_VER happy-$HAPPY_VER cpphs
37+
38+
# installing Agda
39+
# Even if there seems to be duplicated code for master & experimental,
40+
# DO NOT refactor: they regularly get out of sync (typically master
41+
# builds with the released version while experimental uses some dev
42+
# version).
43+
44+
# No matter the path, we should generate a $HOME/installplan.txt to
45+
# check whether the cache needs updating.
46+
47+
- if [[ $TRAVIS_BRANCH = "master" ]]; then
48+
cd ../ &&
49+
git clone https://github.com/agda/agda &&
50+
cd agda &&
51+
git checkout 5053aa9d2a901cfb4c54848e8455820f0183f1b3 &&
52+
cabal install --only-dependencies --dry -v > $HOME/installplan.txt ;
53+
fi
54+
55+
- if [[ $TRAVIS_BRANCH = "experimental" ]]; then
56+
cd ../ &&
57+
git clone https://github.com/agda/agda &&
58+
cd agda &&
59+
git checkout c2d5ec4b2403c68d615b81258d6131774e492797 &&
60+
cabal install --only-dependencies --dry -v > $HOME/installplan.txt ;
61+
fi
62+
63+
# checking whether .ghc is still valid
64+
- sed -i -e '1,/^Resolving /d' $HOME/installplan.txt; cat $HOME/installplan.txt
65+
- touch $HOME/.cabsnap/installplan.txt
66+
- mkdir -p $HOME/.cabsnap/ghc $HOME/.cabsnap/lib $HOME/.cabsnap/share $HOME/.cabsnap/bin
67+
- if diff -u $HOME/.cabsnap/installplan.txt $HOME/installplan.txt;
68+
then
69+
echo "cabal build-cache HIT";
70+
rm -rfv .ghc;
71+
cp -a $HOME/.cabsnap/ghc $HOME/.ghc;
72+
cp -a $HOME/.cabsnap/lib $HOME/.cabsnap/share $HOME/.cabsnap/bin $HOME/.cabal/;
73+
else
74+
echo "cabal build-cache MISS";
75+
rm -rf $HOME/.cabsnap;
76+
mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;
77+
fi
78+
79+
- if [[ $TRAVIS_BRANCH = "master" ]]; then
80+
cabal install ;
81+
fi
82+
83+
- if [[ $TRAVIS_BRANCH = "experimental" ]]; then
84+
cabal install ;
85+
fi
86+
87+
# snapshot package-db on cache miss
88+
- echo "snapshotting package-db to build-cache";
89+
mkdir $HOME/.cabsnap;
90+
cp -a $HOME/.ghc $HOME/.cabsnap/ghc;
91+
cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin $HOME/installplan.txt $HOME/.cabsnap/;
92+
93+
- if [[ $TRAVIS_BRANCH = "master" ]]; then
94+
cd ../ ;
95+
fi
96+
97+
- if [[ $TRAVIS_BRANCH = "experimental" ]]; then
98+
cd ../ ;
99+
fi
100+
101+
# installing fix-whitespace
102+
- git clone https://github.com/agda/fix-whitespace --depth=1
103+
- cd fix-whitespace
104+
- cabal install fix-whitespace.cabal
105+
- cd ../
106+
107+
# generating Everything.agda
108+
- cd agda-stdlib
109+
- cabal install lib.cabal
110+
- runghc GenerateEverything.hs
111+
112+
# setting up travis-specific scripts and files
113+
- cp travis/* .
114+
115+
before_script:
116+
- export AGDA_OPTIONS="-Werror"
117+
- export RTS_OPTIONS="+RTS -M3.5G -H3.5G -A128M -RTS"
118+
119+
script:
120+
# generating index.agda
121+
- ./index.sh
122+
# detecting whitespace violations
123+
- fix-whitespace --check
124+
# expose the value of OPTIONS
125+
- echo $AGDA_OPTIONS
126+
- echo $RTS_OPTIONS
127+
# checking safe modules build with --safe
128+
- agda $AGDA_OPTIONS $RTS_OPTIONS -i . -i src/ --safe EverythingSafeGuardedness.agda
129+
- agda $AGDA_OPTIONS $RTS_OPTIONS -i . -i src/ --safe EverythingSafeSizedTypes.agda
130+
# detecting basic compilation errors
131+
- agda $AGDA_OPTIONS $RTS_OPTIONS -i . -i src/ -c --no-main Everything.agda
132+
# compiling & running the examples using the FFI
133+
- agda $AGDA_OPTIONS $RTS_OPTIONS -i . -i src/ -c README/Foreign/Haskell.agda && ./Haskell
134+
# building the docs
135+
- agda $AGDA_OPTIONS $RTS_OPTIONS -i . -i src/ --html safe.agda
136+
- agda $AGDA_OPTIONS $RTS_OPTIONS -i . -i src/ --html index.agda
137+
138+
# moving everything to the appropriate directory
139+
- if [[ $TRAVIS_BRANCH = "master" ]]; then
140+
mv html/* . ;
141+
fi
142+
- if [[ $TRAVIS_BRANCH = "experimental" ]]; then
143+
mkdir -p experimental ;
144+
mv html/* experimental/ ;
145+
fi
146+
147+
after_success:
148+
# uploading to gh-pages
149+
- git init
150+
- git config --global user.name "Travis CI bot"
151+
- git config --global user.email "[email protected]"
152+
- git remote add upstream https://[email protected]/agda/agda-stdlib.git &>/dev/null
153+
- git fetch upstream && git reset upstream/gh-pages
154+
- if [[ $TRAVIS_BRANCH = "master" ]]; then
155+
git checkout HEAD -- v0.16/ v0.17/ v1.0/ v1.1/ v1.2/ experimental/ ;
156+
fi
157+
- if [[ $TRAVIS_BRANCH = "experimental" ]]; then
158+
git checkout HEAD -- *.html v0.16/ v0.17/ v1.0/ v1.1/ v1.2/ ;
159+
fi
160+
- git add -f \*.html
161+
- git commit -m "Automatic HTML update via Travis"
162+
- if [[ $TRAVIS_PULL_REQUEST = "false" && ($TRAVIS_BRANCH = "master" || $TRAVIS_BRANCH = "experimental") ]]; then
163+
git push -q upstream HEAD:gh-pages &>/dev/null;
164+
fi
165+
166+
notifications:
167+
email: false
168+
169+
- stage: stack
170+
env:
171+
GHC_VER=8.4.4
172+
cache:
173+
directories:
174+
- $HOME/.stack
175+
- $TRAVIS_BUILD_DIR/.stack-work
176+
- $HOME/.local/bin
177+
before_install:
178+
# Install ghc
179+
- sudo -E apt-add-repository -y "ppa:hvr/ghc" &&
180+
travis_apt_get_update &&
181+
sudo -E apt-get -yq --no-install-suggests --no-install-recommends install ghc-${GHC_VER} &&
182+
export PATH=/opt/ghc/$GHC_VER/bin:$PATH
183+
# Install stack
184+
- mkdir -p ~/.local/bin && export PATH=$HOME/.local/bin:$PATH &&
185+
travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
186+
# Set up arguments and flags for stack compilation
187+
- export ARGS="--stack-yaml stack-${GHC_VER}.yaml --no-terminal --system-ghc"
188+
- echo "*** GHC version ***" && ghc --version &&
189+
echo "*** Stack version ***" && stack --version
190+
install:
191+
- stack ${ARGS} build
192+
script:
193+
- stack ${ARGS} exec -- GenerateEverything
194+
- stack ${ARGS} exec -- AllNonAsciiChars
195+
before_cache:
196+
- find ${TRAVIS_BUILD_DIR}/.stack-work -type f -name '*.agdai' -delete
197+
after_success: []

0 commit comments

Comments
 (0)