From 251d9bf751dbda932c6b7390acd31f4231ad0b9b Mon Sep 17 00:00:00 2001 From: Kenichi Asai Date: Fri, 23 Aug 2019 09:25:24 +0900 Subject: [PATCH 1/8] Inference: a variable -> an abstraction --- src/plfa/part2/Inference.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md index e0c9a356..bc3242e7 100644 --- a/src/plfa/part2/Inference.lagda.md +++ b/src/plfa/part2/Inference.lagda.md @@ -168,7 +168,7 @@ checks that the inherited and synthesised types match. Similarly, we said above that the function of an application is typed by synthesis and that abstractions are typed by inheritance, giving a -mismatch if the function of an application is a variable. Hence, we +mismatch if the function of an application is an abstraction. Hence, we need a way to treat an inherited term as if it is synthesised. We introduce a new term form `M ↓ A` for this purpose. The typing judgment returns `A` as the synthesized type of the term as a whole, From fcb5a56fa7e2021ba99b2040f000bd86231315a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Merlin=20G=C3=B6ttlinger?= Date: Tue, 15 Oct 2019 09:56:56 +0200 Subject: [PATCH 2/8] Don't hardcode executable paths `bash` is not specified to reside under `/bin/bash` on all OSs. E.g. on NixOS it does not. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 991d38c1..9f7b534f 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,4 @@ -SHELL := /bin/bash +SHELL := /usr/bin/env bash AGDA := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md') AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai') MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA)))) From 23ab17728d5092059625da1585d8d18d2de32a78 Mon Sep 17 00:00:00 2001 From: Vi Po Date: Sun, 20 Oct 2019 22:25:39 +0300 Subject: [PATCH 3/8] Fix Bit format --- src/plfa/part1/Naturals.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index a2b81f27..dc9cea37 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -913,7 +913,7 @@ between the two representations. from : Bin → ℕ For the former, choose the bitstring to have no leading zeros if it -represents a positive natural, and represent zero by `x0 nil`. +represents a positive natural, and represent zero by `⟨⟩ O`. Confirm that these both give the correct answer for zero through four. ``` From 1615048a3193634322e6ff45c550b184d7fe493f Mon Sep 17 00:00:00 2001 From: Pedro Minicz Date: Mon, 21 Oct 2019 11:41:11 -0300 Subject: [PATCH 4/8] Fix: missing close backquote on inline code. --- src/plfa/part1/Lists.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index 2d01edec..de388e4f 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -656,7 +656,7 @@ Show foldr _∷_ [] xs ≡ xs -Show as a consequence of `foldr-++ above that +Show as a consequence of `foldr-++` above that xs ++ ys ≡ foldr _∷_ ys xs From 93a623ee856af270cdaa5a94b62b4cb5af6e9def Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Mon, 21 Oct 2019 15:47:52 +0100 Subject: [PATCH 5/8] Moved make_assignment to TSPL subdirectory. --- make_assignment.sh => courses/tspl/make_assignment.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename make_assignment.sh => courses/tspl/make_assignment.sh (99%) diff --git a/make_assignment.sh b/courses/tspl/make_assignment.sh similarity index 99% rename from make_assignment.sh rename to courses/tspl/make_assignment.sh index 40b5be3f..85f42911 100755 --- a/make_assignment.sh +++ b/courses/tspl/make_assignment.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # This script can be used to automatically generate assignment files from PLFA source files. # It takes a course abbreviation, e.g. TSPL, a year, and the number of the assignment. From 7f99b5f7856a37a858a59b7490daf10eb9d47ff4 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Mon, 21 Oct 2019 16:22:53 +0100 Subject: [PATCH 6/8] Added script for sending marks. --- courses/tspl/send_marks.sh | 49 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100755 courses/tspl/send_marks.sh diff --git a/courses/tspl/send_marks.sh b/courses/tspl/send_marks.sh new file mode 100755 index 00000000..516c4e73 --- /dev/null +++ b/courses/tspl/send_marks.sh @@ -0,0 +1,49 @@ +#!/usr/bin/env bash + +# Sends out marks for students based on the folder structure used by Submit, +# the coursework submission system used in the School of Informatics at the +# University of Edinburgh. +# +# This script assumes the following folder structure: +# +# $DIR/sXXXXXXX/cw$CW/$FILE +# +# The variable DIR refers to the directory passed in as an argument to the +# script. The variable XXXXXXX refers to the student ID, and it is assumed +# that +# +# sXXXXXXX@sms.ed.ac.uk +# +# is a valid email address. The variable $CW refers to the number for of the +# coursework of which the students are meant to be notified. The directory +# DIR/sXXXXXXX/cwY/ should only contain a single file, which should be +# specified using the FILE parameter. +# +# Usage: +# +# ./send_marks.sh [DIR] [CW] [FILE] + +DIR="$1" +shift + +CW="$1" +shift + +FILE="$1" +shift + +for ATTACHMENT in "${DIR%/}/s"*"/cw$CW/$FILE"; do + SUBJ="Mark for coursework $CW" + BODY="" + SID=$(echo "$ATTACHMENT" | sed 's|.*/\(s[0-9]\{7\}\)/.*|\1|') + ADDR="$SID@sms.ed.ac.uk" + CMD="echo \"$BODY\" | mail -s \"$SUBJ\" -a \"$ATTACHMENT\" \"$ADDR\"" + echo "You are about to run the following command:" + echo -e "\n$CMD\n" + read -p "Are you sure? " -n 1 -r + echo + if [[ $REPLY =~ ^[Yy]$ ]] + then + eval "$CMD" + fi +done From 9604413f20c53281f2c61bef996a0f0dd3554716 Mon Sep 17 00:00:00 2001 From: Orestis Melkonian Date: Tue, 22 Oct 2019 11:30:18 +0100 Subject: [PATCH 7/8] Add myself as a teaching assistant for TSPL'19 --- courses/tspl/2019/tspl2019.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md index ecf759b4..224653d3 100644 --- a/courses/tspl/2019/tspl2019.md +++ b/courses/tspl/2019/tspl2019.md @@ -8,8 +8,9 @@ permalink : /TSPL/2019/ * **Instructor** [Philip Wadler](https://homepages.inf.ed.ac.uk/wadler) -* **Teaching assistant** +* **Teaching assistants** - [Wen Kokke](mailto:wen.kokke@ed.ac.uk) + - [Orestis Melkonian](mailto:o.melkonian@sms.ed.ac.uk) ## Lectures From 3e28965c098c660375c558acef5502ec0891b1de Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Thu, 24 Oct 2019 21:43:09 +0100 Subject: [PATCH 8/8] Update make_assignment script to place exercises from each chapter in their own module, import the chapter and its dependencies, hiding duplicate definitions. --- courses/tspl/make_assignment.sh | 133 +++++++++++++++++++++++++++----- 1 file changed, 115 insertions(+), 18 deletions(-) diff --git a/courses/tspl/make_assignment.sh b/courses/tspl/make_assignment.sh index 85f42911..10f0928f 100755 --- a/courses/tspl/make_assignment.sh +++ b/courses/tspl/make_assignment.sh @@ -1,5 +1,10 @@ #!/usr/bin/env bash +# TODO: +# - put the exercises from each chapter in their own module +# - replicate the imports from that module +# - import that module hiding anything defined in an exercise section + # This script can be used to automatically generate assignment files from PLFA source files. # It takes a course abbreviation, e.g. TSPL, a year, and the number of the assignment. # At the moment, it outputs the University of Edinburgh guidelines for good scholarly practice, @@ -61,31 +66,123 @@ yourself, or your group in the case of group practicals). EOF -## Make import statements +## Awk Scripts -cat <<-EOF +AWK_GET_IMPORTS=' + /^#/ { + import=0 + } + /^## Imports/ { + import=1 + } + /^```/ { + code=!code; + { + if (import) + print $0 + }; + next + } + { + if (import) { + if (code) + print " "$0 + else + print $0 + } + } +' -## Imports +AWK_GET_DEFNS=' + /^#/ { + exercise=0 + } + /^#### Exercise/ { + exercise=1 + } + /^```/ { + code=!code; + next + } + !/^ / { + postulate=0 + } + /^postulate/ { + postulate=1 + } + /^ [^ :(){}]+ +:/ { + if (exercise && code && postulate) + print $0 + } + /^[^ :(){}]+ +:/ { + if (exercise && code) + print $0 + } +' -\`\`\` -EOF -for SRC in "$@"; do - AGDA_MODULE=$(eval "echo \"$SRC\" | sed -e \"s|src/||g; s|\\\.lagda\\\.md||g; s|/|\\\.|g;\"") - echo "open import $AGDA_MODULE" -done -cat <<-EOF -\`\`\` +AWK_GET_EXERCISES=' + /^#/ { + exercise=0 + } + /^#### Exercise/ { + exercise=1 + } + /^```/ { + code=!code; + { + if (exercise) + print $0 + }; + next + } + { + if (exercise) { + if (code) + print " "$0 + else + print $0 + } + } +' -EOF - -## Extract exercises +## Exercises for SRC in "$@"; do + + # Generate Section & Module Header NAME=$(basename "${SRC%.lagda.md}") - cat <<-EOF + echo + echo "## $NAME" + echo + echo '```' + echo "module $NAME where" + echo '```' + echo -## $NAME + # Extract Imports + awk "$AWK_GET_IMPORTS" "$SRC" -EOF - awk '/^#/{flag=0} /^#### Exercise/{flag=1} flag' "$SRC" + # Generate Import and Hiding List + echo '```' + AGDA_MODULE=$(eval "echo \"$SRC\" | sed -e \"s|src/||g; s|\\\.lagda\\\.md||g; s|/|\\\.|g;\"") + echo " open import $AGDA_MODULE" + HIDING_LIST="" + OLDIFS=$IFS + IFS=$(echo -en "\n\b") + for defn in `awk "$AWK_GET_DEFNS" "$SRC"`; + do + NEW=$(eval "echo \"$defn\" | cut -d: -f1 | xargs") + if [ -z "$HIDING_LIST" ]; then + HIDING_LIST="$NEW" + else + HIDING_LIST="$HIDING_LIST; $NEW" + fi + done + IFS=$OLDIFS + echo " hiding ($HIDING_LIST)" + echo '```' + echo + + # Extract Exercises + awk "$AWK_GET_EXERCISES" "$SRC" done