Skip to content

Commit 30479ba

Browse files
pmbittnerpmbittner
authored
Merge pull request #68 from pmbittner/develop
New Release for OOPSLA
2 parents b7b6b2d + 9d04ec6 commit 30479ba

File tree

122 files changed

+6890
-4243
lines changed

Some content is hidden

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

122 files changed

+6890
-4243
lines changed

‎.gitmodules

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
[submodule "agda-stdlib"]
22
path = agda-stdlib
3-
url = git@github.com:agda/agda-stdlib.git
3+
url = https://github.com/agda/agda-stdlib.git

‎Dockerfile

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# syntax=docker/dockerfile:1
2+
3+
# We use Nix for the build.
4+
FROM nixos/nix:2.22.0 AS builder
5+
6+
# Create and navigate to a working directory
7+
WORKDIR /home/user
8+
9+
# Copy all of the source code into the working directory. Impurities like
10+
# additional files and previous build results will be filtered by Nix. Note that
11+
# all files which are considered *tracked* by Git will be used for the build,
12+
# even if they are modified.
13+
COPY . .
14+
15+
# Patch Windows line endings if the repository was cloned on Windows.
16+
RUN nix-shell -p dos2unix --run 'find . -exec dos2unix {} +'
17+
18+
# Verify all proofs and build the demo.
19+
RUN nix-build
20+
21+
# Copy the demo with all runtime dependencies (ignoring build-time dependencies)
22+
# to a separate folder. Such a subset of the Nix store is called a closure and
23+
# enables us to create a minimal Docker container.
24+
RUN mkdir closure
25+
RUN nix-store -qR result | xargs cp -Rt closure
26+
27+
# Start building the final container.
28+
FROM scratch
29+
30+
# Copy the demo (it's runtime closure) to the final container.
31+
COPY --from=builder /home/user/closure /nix/store
32+
33+
# Copy the symlink to the demo derivation, mostly for convenience.
34+
COPY --from=builder /home/user/result /demo
35+
36+
# Enforce a UTF-8 locale to ensure that the Haskell runtime can output all the
37+
# Unicode characters.
38+
ENV LC_ALL=C.UTF-8
39+
40+
CMD ["/demo/bin/Vatras"]

‎EPVL.agda-lib

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1-
name: EPVL
1+
name: Vatras
22
depend: standard-library-2.0
3-
include: src
3+
include: src
4+
flags: --sized-types

‎README.md

Lines changed: 485 additions & 38 deletions
Large diffs are not rendered by default.

‎agda-stdlib

Submodule agda-stdlib updated 809 files

‎default.nix

Lines changed: 12 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -10,20 +10,16 @@
1010
}:
1111
pkgs.agdaPackages.mkDerivation {
1212
version = "1.0";
13-
pname = "EPVL";
14-
src = ./.;
13+
pname = "Vatras";
14+
src = with pkgs.lib.fileset;
15+
toSource {
16+
root = ./.;
17+
fileset = gitTracked ./.;
18+
};
1519

1620
buildInputs = [
17-
(pkgs.agdaPackages.standard-library.overrideAttrs
18-
(oldAttrs: {
19-
version = "1.7.2";
20-
src = pkgs.fetchFromGitHub {
21-
repo = "agda-stdlib";
22-
owner = "agda";
23-
rev = "177dc9e";
24-
hash = "sha256-ovnhL5otoaACpqHZnk/ucivwtEfBQtGRu4/xw4+Ws+c=";
25-
};
26-
}))
21+
pkgs.agdaPackages.standard-library
22+
pkgs.makeWrapper
2723
];
2824

2925
buildPhase = ''
@@ -32,9 +28,11 @@ pkgs.agdaPackages.mkDerivation {
3228
make build
3329
'';
3430

35-
installPhase = ''
31+
postInstall = ''
3632
install -D src/Main "$out/bin/$pname"
33+
wrapProgram "$out/bin/$pname" \
34+
--set LC_ALL C.UTF-8
3735
'';
3836

39-
meta = {description = "On the Expressive Power of Programming Languages";};
37+
meta = {description = "On the Expressive Power of Languages for Static Variability";};
4038
}

‎expected-output.txt

Lines changed: 1260 additions & 0 deletions
Large diffs are not rendered by default.

‎flake.nix

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
{
2+
outputs = inputs: {
3+
packages.x86_64-linux.default = import inputs.self {system = "x86_64-linux";};
4+
overlays.default = final: prev: {
5+
agdaPackages = prev.agdaPackages.overrideScope' (self: super: {
6+
EPVL = import inputs.self {
7+
system = "x86_64-linux";
8+
pkgs = final;
9+
};
10+
});
11+
};
12+
};
13+
}

‎makefile

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
.PHONY: andrun check check-all check-everything build build-2.6.3 run clean
1+
.PHONY: andrun check check-all check-everything build build-2.6.4.3 run clean
22

33
andrun : build run
44

@@ -14,8 +14,8 @@ check-everything: src/Everything.agda
1414
build:
1515
env AGDA_DIR="./libs" agda --compile src/Main.agda
1616

17-
build-2.6.3:
18-
env AGDA_DIR="./libs" agda-2.6.3 --compile src/Main.agda
17+
build-2.6.4.3:
18+
env AGDA_DIR="./libs" agda-2.6.4.3 --compile src/Main.agda
1919

2020
run:
2121
./src/Main

‎nix/README.nix

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
{
2+
sources ? import ./sources.nix,
3+
system ? builtins.currentSystem,
4+
pkgs ?
5+
import sources.nixpkgs {
6+
overlays = [];
7+
config = {};
8+
inherit system;
9+
},
10+
}:
11+
pkgs.runCommand "Vatras-README" {
12+
nativeBuildInputs = [
13+
(pkgs.ruby.withPackages (pkgs: with pkgs; [
14+
github-pages
15+
jekyll-theme-cayman
16+
]))
17+
pkgs.htmlq
18+
pkgs.python3Packages.weasyprint
19+
];
20+
} ''
21+
cat > _config.yml <<EOF
22+
theme: jekyll-theme-cayman
23+
baseurl: root
24+
EOF
25+
26+
cp ${../README.md} README.md
27+
JEKYLL_ENV=production PAGES_REPO_NWO=user/repo JEKYLL_BUILD_REVISION= github-pages build
28+
29+
htmlq -f _site/index.html -r '#skip-to-content' -r 'header a' -r footer > README.html
30+
sed -i '
31+
\|<link .*href="/root/assets/css/style.css?v="| {
32+
a <style type="text/css">
33+
r _site/assets/css/style.css
34+
a #content { max-width: none !important; }
35+
a </style>
36+
d
37+
}
38+
' README.html
39+
40+
# Don't use a temporary file, or all relative links will break.
41+
# https://github.com/Kozea/WeasyPrint/issues/532
42+
htmlq -f README.html -r 'header' -r 'main > p:first-of-type' | weasyprint -u "" -s <(echo '
43+
@page {
44+
size: A4 landscape;
45+
}
46+
47+
@font-face {
48+
font-family: 'DejaVu Sans';
49+
src: url('file://${pkgs.dejavu_fonts}/share/fonts/truetype/DejaVuSans.ttf') format('truetype');
50+
}
51+
@font-face {
52+
font-family: 'DejaVu Sans Mono';
53+
src: url('file://${pkgs.dejavu_fonts}/share/fonts/truetype/DejaVuSansMono.ttf') format('truetype');
54+
}
55+
@font-face {
56+
font-family: 'DejaVu Serif';
57+
src: url('file://${pkgs.dejavu_fonts}/share/fonts/truetype/DejaVuSerif.ttf') format('truetype');
58+
}
59+
@font-face {
60+
font-family: 'Liberation Mono';
61+
src: url('file://${pkgs.liberation_ttf}/share/fonts/truetype/LiberationMono-Regular.ttf') format('truetype');
62+
}
63+
@font-face {
64+
font-family: 'Liberation Sans';
65+
src: url('file://${pkgs.liberation_ttf}/share/fonts/truetype/LiberationSans-Regular.ttf') format('truetype');
66+
}
67+
@font-face {
68+
font-family: 'Tex Gyre Cursor';
69+
src: url('file://${pkgs.gyre-fonts}/share/fonts/truetype/texgyrecursor-regular.otf') format('opentype');
70+
}
71+
@font-face {
72+
font-family: 'Tex Gyre Heros';
73+
src: url('file://${pkgs.gyre-fonts}/share/fonts/truetype/texgyreheros-regular.otf') format('opentype');
74+
}
75+
') - README.pdf
76+
77+
mkdir "$out"
78+
cp README.html "$out/README.html"
79+
cp README.pdf "$out/README.pdf"
80+
81+
runHook postInstall
82+
''

‎nix/github-workflow-dependencies.nix

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88
inherit system;
99
},
1010
}: let
11-
EPVL = import ../default.nix {};
11+
Vatras = import ../default.nix {};
1212
in
1313
pkgs.mkShell {
14-
inputsFrom = [EPVL];
14+
inputsFrom = [Vatras];
1515
}

‎nix/sources.json

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@
55
"homepage": null,
66
"owner": "NixOS",
77
"repo": "nixpkgs",
8-
"rev": "4ecab3273592f27479a583fb6d975d4aba3486fe",
9-
"sha256": "10wn0l08j9lgqcw8177nh2ljrnxdrpri7bp0g7nvrsn9rkawvlbf",
8+
"rev": "fd281bd6b7d3e32ddfa399853946f782553163b5",
9+
"sha256": "1hy81yj2dcg6kfsm63xcqf8kvigxglim1rcg1xpmy2rb6a8vqvsj",
1010
"type": "tarball",
11-
"url": "https://github.com/NixOS/nixpkgs/archive/4ecab3273592f27479a583fb6d975d4aba3486fe.tar.gz",
11+
"url": "https://github.com/NixOS/nixpkgs/archive/fd281bd6b7d3e32ddfa399853946f782553163b5.tar.gz",
1212
"url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
1313
}
1414
}

‎scripts/find-inconsistency-sources.sh

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
#!/usr/bin/env bash
2+
3+
cd "$(dirname ${BASH_SOURCE[0]})/.."
4+
5+
possible-inconsistencies() {
6+
echo 'postulates:'
7+
grep 'postulate' -r src --include '*agda*'
8+
9+
echo
10+
echo 'terminating pragmas:'
11+
grep 'TERMINATING' -r src --include '*agda*'
12+
13+
echo
14+
echo 'holes:'
15+
(
16+
grep -F '{!' -r src --include '*agda*'
17+
grep ' ?\( \|$\)' -r src --include '*agda*'
18+
)
19+
}
20+
21+
with-doc() {
22+
# Used for alignment.
23+
# Cannot use 'column' because it doesn't exist on MAC.
24+
columnCount="$(possible-inconsistencies | awk 'BEGIN { max=0 } { if (max < length($0)) max=length($0) } END { print max }')"
25+
26+
POSIXLY_CORRECT=1 awk '
27+
BEGIN {
28+
doc[""]=""
29+
doc["postulates:"]=""
30+
doc["terminating pragmas:"]=""
31+
doc["holes:"]=""
32+
33+
doc["src/Util/String.agda: where postulate trustMe : _"]="Also proposed in the Agda issue tracker to make String propositions provable. Only used in examples."
34+
# Note: this above postulate appears four times
35+
doc["src/Show/Lines.agda:{-# NON_TERMINATING #-}"]="Only used for printing and thus not proof relevant. Also, NON_TERMINATING functions do not reduce during type checking."
36+
doc["src/Tutorial/A_NewLanguage.lagda.md:We are using the `{-# TERMINATING -#}` flag here:"]="This is actually a comment."
37+
doc["src/Tutorial/A_NewLanguage.lagda.md:{-# TERMINATING #-}"]="Simplification of the tutorial. Not used in the anything else."
38+
doc["src/Tutorial/A_NewLanguage.lagda.md:MyConfig = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
39+
doc["src/Tutorial/A_NewLanguage.lagda.md:⟦_⟧ = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
40+
doc["src/Tutorial/B_Translation.lagda.md:conf e c²ᶜᶜ = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
41+
doc["src/Tutorial/B_Translation.lagda.md:fnoc e cᵐʸ = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
42+
doc["src/Tutorial/B_Translation.lagda.md:preservation-⊆[] e c = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
43+
doc["src/Tutorial/B_Translation.lagda.md:preservation-⊇[] e c = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
44+
doc["src/Tutorial/B_Translation.lagda.md:translate (D ⟨ l , r ⟩) = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
45+
doc["src/Tutorial/B_Translation.lagda.md:translate (a -< cs >-) = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
46+
doc["src/Tutorial/C_Proofs.lagda.md: {!!} -- write down the proof of correctness in this hole"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
47+
doc["src/Tutorial/C_Proofs.lagda.md: {!!} , -- write down the expression in this hole"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
48+
doc["src/Tutorial/C_Proofs.lagda.md:2CC≽MyLang = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
49+
doc["src/Tutorial/C_Proofs.lagda.md:MyLang-is-Sound = {!!}"]="Intentional hole to be filled by you! Not used in anything other than the tutorial."
50+
51+
exitCode=0
52+
}
53+
54+
{
55+
padding='"$columnCount"' - length($0) + 3
56+
if ($0 in doc) {
57+
printf "%s% *s%s\n", $0, padding, "", doc[$0]
58+
} else {
59+
printf "\033[30;41m%s% *s%s\033[39;49m\n", $0, padding, "", "UNDOCUMENTED!!!"
60+
exitCode=1
61+
}
62+
}
63+
64+
END {
65+
exit exitCode
66+
}
67+
'
68+
}
69+
70+
if [ "$1" = "--with-documentation" ]
71+
then
72+
possible-inconsistencies | with-doc
73+
exitCode=$?
74+
else
75+
possible-inconsistencies
76+
exitCode=$?
77+
fi
78+
79+
echo
80+
echo "Hint: Use '$0 --with-documentation | less -S' to be able to see documentation to each source and to scroll horizontally"
81+
82+
exit $exitCode

‎src/Axioms/Extensionality.agda

Lines changed: 0 additions & 28 deletions
This file was deleted.

‎src/Construct/Artifact.agda

Lines changed: 0 additions & 23 deletions
This file was deleted.

0 commit comments

Comments
 (0)