-
Notifications
You must be signed in to change notification settings - Fork 233
Commit
- Loading branch information
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
$%7 �"6�����_T�X�Nݤ�Pp�~*��'���O^6<�W�)aQ� A�k��_�9�c�-��)h���fF��ה�9�C>_�[��AYo@o����%6�7����4����u��g������T�%��"��;�B�v`�Rf����o | ||
This comment has been minimized.
Sorry, something went wrong.
This comment has been minimized.
Sorry, something went wrong.
gallais
Author
Member
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,52 @@ | ||
language: haskell | ||
branches: | ||
only: | ||
- master | ||
|
||
before_install: | ||
# Decrypting the dropbox credentials | ||
- openssl aes-256-cbc -K $encrypted_3f6e0f4132ed_key -iv $encrypted_3f6e0f4132ed_iv -in .dropbox_uploader.enc -out .dropbox_uploader -d | ||
- cp .dropbox_uploader $HOME/ | ||
|
||
install: | ||
# Installing the dropbox download script | ||
- cd $HOME | ||
- curl "https://raw.githubusercontent.com/andreafabrizi/Dropbox-Uploader/master/dropbox_uploader.sh" -o dropbox_uploader.sh | ||
- chmod +x dropbox_uploader.sh | ||
# downloading the last (latest?) tarball and installing agda | ||
- AGDATAR=$(./dropbox_uploader.sh list | tail -n 1 | sed 's/^.*\(Agda.*\)$/\1/') | ||
- ./dropbox_uploader.sh download $AGDATAR . | ||
- tar -xzvf $AGDATAR | ||
- cd $( basename $AGDATAR .tar.gz ) | ||
- sudo ./deploy.sh | ||
# generating Everything.agda | ||
- cabal install filemanip | ||
- cd $HOME/build/gallais/agda-stdlib | ||
- runghc GenerateEverything.hs | ||
|
||
script: | ||
# generating index.agda | ||
- ./index.sh | ||
# building the docs | ||
- agda -i . -i src/ --html src/index.agda | ||
# moving everything at the root | ||
- mv html/* . | ||
|
||
after_success: | ||
# uploading to gh-pages | ||
- git init | ||
- git config --global user.name "Travis CI bot" | ||
- git config --global user.email "travis-ci-bot@travis.fake" | ||
- git remote add upstream https://$GH_TOKEN@github.com/gallais/agda-stdlib.git &>/dev/null | ||
- git fetch upstream && git reset upstream/gh-pages | ||
- git add -f \*.html | ||
- git commit -m "Automatic HTML update via Travis" | ||
- git push -q upstream HEAD:gh-pages &>/dev/null | ||
|
||
notifications: | ||
email: false | ||
|
||
# Github token | ||
env: | ||
global: | ||
secure: f0GRSKTlAw6FdrvkI8LjP5ZhwcGBltJ1t5+nxipqfoR3VczMxcNgXD7bdwtUojFYR48jMs2W+LxEoJcuSH4bsdCeoSfpZ0nU424MDajGh0wuhAbSYKQXPWjFOxwMgC23sCySKhDAZiqN/Wd6orwV1p5JhuJkSCHdVeyUp+hLvIw= |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
for i in $( find src -name "*.agda" | grep -v "index.agda" | sed 's/src\/\(.*\)\.agda/\1/' | sed 's/\//\./g' | sort ); do | ||
echo "import $i" >> src/index.agda; | ||
done |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
module index where | ||
|
||
-- You probably want to start with this module: | ||
import README | ||
|
||
-- For a brief presentation of every single module, head over to | ||
import Everything | ||
|
||
-- Otherwise, here is an exhaustive, stern list of all the available modules: |
2 comments
on commit 532c76f
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
G., src/index.agda is malformed as input for GenerateEverything.hs. Currently, all travis builds of agda are broken:
https://travis-ci.org/agda/agda/jobs/47782771
======================================================================
========================== Standard library ==========================
======================================================================
GenerateEverything.hs: src/index.agda is malformed.
make: *** [library-test] Error 1
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Right, I had patched GenerateEverything on my fork but forgot to include the relevant changes here.
6c97b36 should fix the issue. I hope I haven't forgotten anything else.
Should this file be here??