Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add workflows to check broken links and deploy papers to GH Pages #6236

Merged
merged 16 commits into from
Jun 26, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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}"