Skip to content

Commit ffae2e3

Browse files
authored
Merge pull request #44 from idris-hackers/feature/fix-pdf
Fix PDF
2 parents a112706 + b38a117 commit ffae2e3

17 files changed

+293
-233
lines changed

.gitignore

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -189,3 +189,7 @@ TSWLatexianTemp*
189189
## Generated LaTeX files:
190190
*.tex
191191
src/auto/
192+
193+
194+
## Nix
195+
/result*

.travis.yml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
language: nix
2+
# FIXME: Why does pandoc fail in nix-build?
3+
script: nix-shell --pure --run make

CONTRIBUTING.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,6 @@ the `all.pdf`, `all.tex` and `%.tex` rules in [`src/Makefile`].
169169
[glossaries package]: https://www.ctan.org/pkg/glossaries
170170
[glossary.tex]: https://github.com/idris-hackers/software-foundations/blob/master/src/glossary.tex
171171
[`src/Makefile`]: https://github.com/idris-hackers/software-foundations/blob/master/src/glossary.tex
172-
[PDF]: https://idris-hackers.github.io/software-foundations/pdf/sf-idris-2016.pdf
172+
[PDF]: https://idris-hackers.github.io/software-foundations/pdf/sf-idris-2018.pdf
173173
[Pandoc]: http://pandoc.org
174174
[latexmk]: https://www.ctan.org/pkg/latexmk/

LICENSE

Lines changed: 20 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,20 @@
1-
I hereby assign copyright in my past and future contributions to the Software
2-
Foundations project to the Author of Record of each volume or component, to be
3-
licensed under the same terms as the rest of Software Foundations. I understand
4-
that, at present, the Authors of Record are as follows: For Volumes 1 and 2,
5-
known until 2016 as "Software Foundations" and from 2016 as (respectively)
6-
"Logical Foundations" and "Programming Foundations," the Author of Record is
7-
Benjamin Pierce. For Volume 3, "Verified Functional Algorithms", the Author of
8-
Record is Andrew W. Appel. For components outside of designated Volumes (e.g.,
9-
typesetting and grading tools and other software infrastructure), the Author of
10-
Record is Benjamin Pierce. For the Idris translation, the Author of Record is
11-
Eric Bailey.
1+
The MIT License (MIT)
2+
Copyright © 2016-2018 idris-hackers team
3+
4+
Permission is hereby granted, free of charge, to any person obtaining a copy
5+
of this software and associated documentation files (the “Software”), to deal
6+
in the Software without restriction, including without limitation the rights
7+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8+
copies of the Software, and to permit persons to whom the Software is
9+
furnished to do so, subject to the following conditions:
10+
11+
The above copyright notice and this permission notice shall be included in
12+
all copies or substantial portions of the Software.
13+
14+
THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20+
THE SOFTWARE.

Makefile

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
1-
PKG := software_foundations
2-
3-
4-
# TODO: Find idris executable.
5-
IDRIS ?= idris
1+
PKG := software_foundations
2+
PREFIX ?= docs
3+
IDRIS ?= idris
4+
PDF ?= sf-idris-2018.pdf
65

76

87
.PHONY: pdf site
@@ -21,7 +20,7 @@ check:
2120

2221
pdf:
2322
$(MAKE) -C src
24-
mv src/all.pdf docs/pdf/sf-idris-2016.pdf
23+
mv src/all.pdf docs/pdf/${PDF}
2524

2625

2726
clean-all: clean clean-docs
@@ -40,6 +39,10 @@ site: docs/index.html
4039

4140

4241
docs/index.html: README.md CONTRIBUTING.md
43-
pandoc -f markdown_github -t markdown_github \
44-
-A CONTRIBUTING.md $< \
45-
| pandoc -f markdown_github -t html -s -o $@
42+
pandoc -f gfm -t gfm -A CONTRIBUTING.md $< | \
43+
pandoc -M title='Software Foundations in Idris' \
44+
-f gfm -t html -s -o $@
45+
46+
47+
install:
48+
install -m644 -Dt "${PREFIX}" docs/pdf/${PDF}

README.md

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
# _[Software Foundations][SF] in Idris_
22

3+
[![Build Status](https://travis-ci.org/idris-hackers/software-foundations.svg?branch=develop)](https://travis-ci.org/idris-hackers/software-foundations)
4+
35
:book: [Download the PDF][PDF]
46

57

@@ -37,7 +39,7 @@ Others may work, but here are the versions I'm using.
3739
<!-- Named Links -->
3840

3941
[SF]: http://www.cis.upenn.edu/%7Ebcpierce/sf/current/index.html
40-
[PDF]: https://idris-hackers.github.io/software-foundations/pdf/sf-idris-2016.pdf
42+
[PDF]: https://idris-hackers.github.io/software-foundations/pdf/sf-idris-2018.pdf
4143
[prereqs]: #prerequisites
4244
[GHC]: https://www.haskell.org/ghc/
4345
[Idris]: https://www.idris-lang.org

VERSION

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
0.0.2.0

default.nix

Lines changed: 73 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1,37 +1,85 @@
1-
{ nixpkgs ? import <nixpkgs> {}
2-
, compiler ? "ghc802"
3-
}:
4-
51
let
6-
inherit (nixpkgs) pkgs;
72

8-
haskellPackages = pkgs.haskell.packages."${compiler}";
9-
ghc = haskellPackages.ghcWithPackages (ps: with ps; [
10-
idris
11-
pandoc
12-
]);
13-
# FIXME: TeX Live is pretty much broken in Nix right now.
14-
# xelatex = pkgs.texlive.combine {
15-
# inherit (pkgs.texlive) scheme-small xetex latexmk todonotes;
16-
# };
3+
fetchTarballFromGitHub =
4+
{ owner, repo, rev, sha256, ... }:
5+
builtins.fetchTarball {
6+
url = "https://github.com/${owner}/${repo}/tarball/${rev}";
7+
inherit sha256;
8+
};
9+
10+
fromJSONFile = f: builtins.fromJSON (builtins.readFile f);
11+
1712
in
1813

19-
pkgs.stdenv.mkDerivation rec {
20-
name = "software-foundations-${version}-env";
21-
version = "0.0.1.0";
14+
{ nixpkgs ? fetchTarballFromGitHub (fromJSONFile ./nixpkgs-src.json) }:
15+
16+
with import nixpkgs {
17+
overlays = [
18+
(self: super: {
19+
ghc-with-pandoc = super.haskellPackages.ghcWithPackages (ps: with ps; [
20+
pandoc
21+
]);
22+
23+
idris = with super.idrisPackages; with-packages [
24+
base
25+
prelude
26+
pruviloj
27+
];
2228

29+
xelatex = super.texlive.combine {
30+
inherit (super.texlive) scheme-small
31+
amsmath
32+
datatool
33+
dirtytalk
34+
ebproof
35+
fontspec
36+
framed
37+
fvextra
38+
glossaries
39+
ifplatform
40+
latexmk
41+
lm-math
42+
mfirstuc
43+
minted
44+
newunicodechar
45+
substr
46+
todonotes
47+
xetex
48+
xfor
49+
xindy
50+
xstring;
51+
};
52+
})
53+
];
54+
};
55+
56+
stdenv.mkDerivation rec {
57+
name = "software-foundations-${version}-env";
58+
version = builtins.readFile ./VERSION;
2359
src = ./.;
2460

25-
# TODO: xelatex
26-
buildInputs = [ ghc ] ++
27-
(with pkgs; [ python3 ]) ++
28-
(with pkgs.python35Packages; [ pygments ]);
61+
FONTCONFIG_FILE = makeFontsConf {
62+
fontDirectories = [
63+
iosevka
64+
];
65+
};
66+
67+
buildInputs = [
68+
ghc-with-pandoc
69+
idris
70+
python3Packages.pygments
71+
xelatex
72+
which
73+
];
74+
75+
installFlags = [
76+
"PREFIX=$(out)"
77+
];
2978

30-
meta = with pkgs.stdenv.lib; {
79+
meta = with stdenv.lib; {
3180
description = "Software Foundations in Idris";
32-
# TODO: longDescription
33-
homepage = http://idris-hackers.github.io/software-foundations;
34-
# TODO: license
81+
homepage = https://idris-hackers.github.io/software-foundations;
82+
license = licenses.mit;
3583
maintainers = with maintainers; [ yurrriq ];
3684
inherit (ghc.meta) platforms;
3785
};

0 commit comments

Comments
 (0)