Skip to content

Commit

Permalink
Add workflows to check broken links and deploy papers to GH Pages (#6236
Browse files Browse the repository at this point in the history
)

* Add workflows to check broken links and deploy papers to GH Pages
  • Loading branch information
zeme-wana authored Jun 26, 2024
1 parent 6900c42 commit 5579d34
Show file tree
Hide file tree
Showing 10 changed files with 121 additions and 14 deletions.
33 changes: 33 additions & 0 deletions .github/workflows/broken-links.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
# This job checks for broken links in the various files.

name: "🔗 Broken Links"

on:
schedule:
- cron: 0 0 * * * # Daily at midnight
workflow_dispatch: # Or manually dispatch the job
pull_request:
paths:
- .github/ISSUE_TEMPLATE/bug_report.yml
- .github/ISSUE_TEMPLATE/feature_request.yml
- .github/PULL_REQUEST_TEMPLATE.md
- .github/SECURITY.md
- CODE_OF_CONDUCT.md
- CONTRIBUTING.adoc
- LICENSE
- NOTICE
- README.adoc
- RELEASE.adoc
- STYLEGUIDE.adoc

jobs:
check:
name: Check
runs-on: [plutus-shared, self-hosted]
steps:
- name: Checkout
uses: actions/checkout@main

- name: Run Linkchecker
run: |
nix develop --no-warn-dirty --accept-flake-config --command ./scripts/check-broken-links.sh
1 change: 1 addition & 0 deletions .github/workflows/cost-model-benchmark.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ jobs:
run:
name: Run
runs-on: [self-hosted, plutus-benchmark]
timeout-minutes: 14400
steps:
- name: Checkout
uses: actions/checkout@main
Expand Down
45 changes: 45 additions & 0 deletions .github/workflows/papers-and-specs.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
# This job builds various papers and deploys them to:
# https://intersectmbo.github.io/plutus/resources

name: "📝 Papers & Specs"

on:
pull_request:
workflow_dispatch:

jobs:
deploy:
name: Deploy
runs-on: [self-hosted, plutus-shared]
permissions:
contents: write
environment:
name: github-pages
steps:
- name: Checkout
uses: actions/checkout@main

- name: Build Papers
run: |
TARGETS=(
plutus-report
plutus-core-spec
extended-utxo-spec
unraveling-recursion-paper
system-f-in-agda-paper
eutxo-paper
utxoma-paper
eutxoma-paper
)
mkdir -p _resources
for target in "${TARGETS[@]}"; do
nix build --no-warn-dirty --accept-flake-config .#latex-documents.x86_64-linux.${target}
cp -fr ./result/*.pdf _resources/${target}.pdf
done
- name: Publish Papers
uses: JamesIves/[email protected]
with:
folder: _resources
target-folder: resources
single-commit: true
16 changes: 8 additions & 8 deletions README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -55,17 +55,17 @@ The documentation for the metatheory can be found https://intersectmbo.github.io

=== Specifications and design

- https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.plutus-report/latest/download/1[Plutus Technical Report (draft)]: a technical report and design document for the project.
- https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.plutus-core-spec/latest/download/1[Plutus Core Specification]: the formal specification of the core language.
- https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.extended-utxo-spec/latest/download/1[Extended UTXO Model]: a design document for the core changes to the Cardano ledger.
- https://intersectmbo.github.io/plutus/resources/plutus-report.pdf[Plutus Technical Report (draft)]: a technical report and design document for the project.
- https://intersectmbo.github.io/plutus/resources/plutus-core-spec.pdf[Plutus Core Specification]: the formal specification of the core language.
- https://intersectmbo.github.io/plutus/resources/extended-utxo-spec.pdf[Extended UTXO Model]: a design document for the core changes to the Cardano ledger.

=== Academic papers

- https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.unraveling-recursion-paper/latest/download/1[Unraveling Recursion]: a description of some of the compilation strategies used in Plutus IR (https://doi.org/10.1007/978-3-030-33636-3_15[published version]).
- https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.system-f-in-agda-paper/latest/download/1[System F in Agda]: a formal model of System F in Agda (https://doi.org/10.1007/978-3-030-33636-3_10[published version]).
- https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.eutxo-paper/latest/download/1[The Extended UTXO Model]: a full presentation of the EUTXO ledger extension (https://doi.org/10.1007/978-3-030-54455-3_37[published version]).
- https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.utxoma-paper/latest/download/1[UTXOma: UTXO with Multi-Asset Support]: a full presentation of the multi-asset ledger extension (https://doi.org/10.1007/978-3-030-61467-6_8[published version]).
- https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.eutxoma-paper/latest/download/1[Native Custom Tokens in the Extended UTXO Model]: a discussion of the interaction of the multi-asset support with EUTXO (https://doi.org/10.1007/978-3-030-61467-6_7[published version]).
- https://intersectmbo.github.io/plutus/resources/unraveling-recursion-paper.pdf[Unraveling Recursion]: a description of some of the compilation strategies used in Plutus IR (https://doi.org/10.1007/978-3-030-33636-3_15[published version]).
- https://intersectmbo.github.io/plutus/resources/system-f-in-agda-paper.pdf[System F in Agda]: a formal model of System F in Agda (https://doi.org/10.1007/978-3-030-33636-3_10[published version]).
- https://intersectmbo.github.io/plutus/resources/eutxo-paper.pdf[The Extended UTXO Model]: a full presentation of the EUTXO ledger extension (https://doi.org/10.1007/978-3-030-54455-3_37[published version]).
- https://intersectmbo.github.io/plutus/resources/utxoma-paper.pdf[UTXOma: UTXO with Multi-Asset Support]: a full presentation of the multi-asset ledger extension (https://doi.org/10.1007/978-3-030-61467-6_8[published version]).
- https://intersectmbo.github.io/plutus/resources/eutxoma-paper.pdf[Native Custom Tokens in the Extended UTXO Model]: a discussion of the interaction of the multi-asset support with EUTXO (https://doi.org/10.1007/978-3-030-61467-6_7[published version]).
- https://arxiv.org/abs/2201.04919[Translation Certification for Smart Contracts]: a certifier of Plutus IR compiler passes written in Coq.

== Licensing
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -36,4 +36,4 @@ Supporting "mixed" code in this way enables libraries written with the Plutus Ha

The formal details of Plutus Core are in its [specification](https://github.com/IntersectMBO/plutus#specifications-and-design).

The design is discussed in the [technical report](https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.plutus-report/latest/download/1).
The design is discussed in the [technical report](https://intersectmbo.github.io/plutus/resources/plutus-report.pdf).
2 changes: 1 addition & 1 deletion doc/docusaurus/docs/essential-concepts/plutus-platform.mdx
Original file line number Diff line number Diff line change
Expand Up @@ -87,5 +87,5 @@ Even simple applications must deal with this complexity, and for more advanced a

- Michael Peyton-Jones and Jann Mueller introduce the Plutus platform in [this session](https://youtu.be/usMPt8KpBeI?si=4zkS3J7Bq8aFxWbU) from the Cardano 2020 event.

- The design of the platform is discussed in the [Plutus technical report](https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.plutus-report/latest/download/1).
- The design of the platform is discussed in the [Plutus technical report](https://intersectmbo.github.io/plutus/resources/plutus-report.pdf).

2 changes: 1 addition & 1 deletion doc/plutus-core-spec/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ This directory contains a draft of a version of the Plutus Core specification
updated so that the language is parametric over a collection of built-in types
and functions. It also updates the specification to reflect the fact that
built-in functions can now be partially applied. ~Click
[here](https://ci.iog.io/job/input-output-hk-plutus/master/x86_64-linux.packages.plutus-core-spec/latest/download/1)
[here](https://intersectmbo.github.io/plutus/resources/plutus-core-spec.pdf)
to open a PDF of the most recent version of the specification in the main branch
of this repository.~ The link given in the previous sentence currently appears to be broken: would-be readers should build the PDF themselves. On a Linux system, `make` in the main source directory should do this.

Expand Down
2 changes: 1 addition & 1 deletion plutus-core/docs/BuiltinsOverview.md
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ toBuiltinMeaning
-> BuiltinMeaning val (CostingPart uni fun)
```

i.e. in order to construct a `BuiltinMeaning` one needs not only a built-in function, but also a semantics variant (a "version") of the set of built-in functions. You can read more about versioning of builtins and everything else in [CIP-35](https://cips.cardano.org/cips/cip35) and in Chapter 4 of the Plutus Core [specification](https://ci.iog.io/build/834321/download/1/plutus-core-specification.pdf).
i.e. in order to construct a `BuiltinMeaning` one needs not only a built-in function, but also a semantics variant (a "version") of the set of built-in functions. You can read more about versioning of builtins and everything else in [CIP-35](https://cips.cardano.org/cips/cip35) and in Chapter 4 of the Plutus Core [specification](https://intersectmbo.github.io/plutus/resources/plutus-core-spec.pdf#page=8).

We do not construct `BuiltinMeaning`s manually, because that would be extremely laborious. Instead, we use an auxiliary function that does the heavy lifting for us. Here's its type signature with a few lines of constraints omitted for clarity:

Expand Down
4 changes: 2 additions & 2 deletions plutus-metatheory/src/Type/RenamingSubstitution.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ variable
As we are going to push renamings through types we need to be able to push them
under a binder. To do this safely the newly bound variable should remain untouched and
other renamings should be shifted by one to accommodate this. (Note: this is
called `lift⋆` in the [paper](https://ci.iog.io/build/1230848/download/1/paper.pdf#page=8) ).
called `lift⋆` in the [paper](https://intersectmbo.github.io/plutus/resources/plutus-core-spec.pdf#page=8) ).

```
ext : Ren Φ Ψ
Expand Down Expand Up @@ -252,7 +252,7 @@ variable
σ σ' : Sub Φ Ψ
```

Extending a type substitution — used when going under a binder. (This is called `lifts` in the [paper](https://ci.iog.io/build/1230848/download/1/paper.pdf#page=8) ).
Extending a type substitution — used when going under a binder. (This is called `lifts` in the [paper](https://intersectmbo.github.io/plutus/resources/plutus-core-spec.pdf#page=8) ).

```
exts : Sub Φ Ψ
Expand Down
28 changes: 28 additions & 0 deletions scripts/check-broken-links.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
TARGETS=(
.github/ISSUE_TEMPLATE/bug_report.yml
.github/ISSUE_TEMPLATE/feature_request.yml
.github/PULL_REQUEST_TEMPLATE.md
.github/SECURITY.md
CODE_OF_CONDUCT.md
CONTRIBUTING.adoc
LICENSE
NOTICE
README.adoc
RELEASE.adoc
STYLEGUIDE.adoc
)

FAILED=0

for file in "${TARGETS[@]}"; do
echo "Checking ${file}"
grep -oE "\b(https?://|www\.)[^\[\(\)\"]+\b" "${file}" \
| linkchecker --no-warnings --recursion-level 0 --output failures --check-extern --stdin \
--ignore-url https://img.shields.io/matrix/plutus-core%3Amatrix.org # For some reason linkchecker fails to check this URL though it is valid
if [ $? -ne 0 ]; then
echo "${file} has broken links, see output above"
FAILED=1
fi
done

exit "${FAILED}"

0 comments on commit 5579d34

Please sign in to comment.