From 2cda5ea939129b948acdd76df624ff602d13a40a Mon Sep 17 00:00:00 2001 From: zeme Date: Fri, 5 Jul 2024 11:46:27 +0200 Subject: [PATCH 1/8] Action for checking broken links everywhere --- .github/actions/linkchecker/action.yml | 81 ++++++++++++++++++++++++++ .github/workflows/broken-links.yml | 31 ++++++++-- 2 files changed, 107 insertions(+), 5 deletions(-) create mode 100644 .github/actions/linkchecker/action.yml diff --git a/.github/actions/linkchecker/action.yml b/.github/actions/linkchecker/action.yml new file mode 100644 index 00000000000..be894c3e495 --- /dev/null +++ b/.github/actions/linkchecker/action.yml @@ -0,0 +1,81 @@ +name: Run Linkchecker + +description: | + Run linkchecker on a URL or a list of files. + This only checks external links. + +inputs: + target-url: + default: "" + description: | + Target url to check for external broken links. + Either this or target-url must be non-empty, not both. + + target-files: + default: "" + description: | + String of space-separated target filepath patterns. + Each pattern will be fed to find using the -name directive. + URLs beginning with "https?" will be regex-matched and extracted from each file. + Either this or target-url must be non-empty, not both. + + ignore-urls: + default: "" + description: | + String of space-separated URL patterns to ignore. + Each URL is fed to linkchecker using the --ignore-url option. + +runs: + using: "composite" + steps: + - name: Check Valid Inputs + if: ${{ inputs.target-url == "" && inputs.target-files == "" || inputs.target-url != "" && inputs.target-files != ""}} + run: + echo "Provide a value for either target-url xor target-files." + exit 1 + + - name: Checkout Repo + if: ${{ inputs.target-url != "" }} + uses: actions/checkout@main + + - name: Check URL + if: ${{ inputs.target-url != "" }} + run: | + linkchecker + echo "Collecting --ignore-url options" + IGNORE_URL_OPTIONS=() + for failure in "${BROKEN_LINKS[@]}"; do + url="${failure##* }" + IGNORE_URL_OPTIONS+=("--ignore-url=${url}") + done + +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}" + + + - name: Check Files + if: ${{ inputs.target-files != "" }} + run: | + 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}" \ No newline at end of file diff --git a/.github/workflows/broken-links.yml b/.github/workflows/broken-links.yml index 5fcf01ec61e..7ef2bf44fa9 100644 --- a/.github/workflows/broken-links.yml +++ b/.github/workflows/broken-links.yml @@ -1,5 +1,9 @@ -# This job checks for broken links in the various files. - +# This job checks for broken links in the various places: +# - The live haddock site +# - The live metatheory site +# - The live docusaurus site +# - Anchors and URLs in various files in the repo + name: "🔗 Broken Links" on: @@ -21,13 +25,30 @@ on: - STYLEGUIDE.adoc jobs: - check: - name: Check + repo-files: + name: Repo Files + 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 + + + haddock-site: + name: Haddock Site runs-on: [plutus-shared, self-hosted] steps: - name: Checkout uses: actions/checkout@main - name: Run Linkchecker + env: + IGNORE_URLS: run: | - nix develop --no-warn-dirty --accept-flake-config --command ./scripts/check-broken-links.sh \ No newline at end of file + nix develop --no-warn-dirty --accept-flake-config --command ./scripts/check-broken-links.sh + + + From 362a4fda5c0659b6e6f8405ec95f582cd016ee3b Mon Sep 17 00:00:00 2001 From: zeme Date: Mon, 8 Jul 2024 09:13:32 +0200 Subject: [PATCH 2/8] wip --- .github/ISSUE_TEMPLATE/bug_report.yml | 2 +- .github/ISSUE_TEMPLATE/feature_request.yml | 2 +- .github/actions/linkchecker/action.yml | 81 ------------------- .github/workflows/broken-links.yml | 42 ++-------- .github/workflows/docusaurus-site.yml | 13 ++- .github/workflows/haddock-site.yml | 21 +++-- .github/workflows/longitudinal-benchmark.yml | 4 +- .github/workflows/metatheory-site.yml | 18 +++-- .github/workflows/papers-and-specs.yml | 2 +- README.adoc | 22 ++--- doc/docusaurus/README.md | 2 +- .../essential-concepts/plutus-foundation.md | 2 +- .../essential-concepts/plutus-platform.mdx | 2 +- doc/docusaurus/docs/index.md | 6 +- .../docs/reference/haddock-documentation.md | 10 +-- doc/docusaurus/docusaurus.config.ts | 7 +- doc/plutus-core-spec/README.md | 2 +- doc/read-the-docs-site/README.md | 4 +- plutus-core/docs/BuiltinsOverview.md | 2 +- plutus-metatheory/README.md | 76 ++++++++--------- plutus-metatheory/src/Builtin.lagda.md | 6 +- .../src/Type/RenamingSubstitution.lagda.md | 4 +- scripts/check-broken-links.sh | 33 ++++---- scripts/combined-haddock.sh | 2 +- 24 files changed, 140 insertions(+), 225 deletions(-) delete mode 100644 .github/actions/linkchecker/action.yml diff --git a/.github/ISSUE_TEMPLATE/bug_report.yml b/.github/ISSUE_TEMPLATE/bug_report.yml index ffe7f2bfdea..bb6d258c73c 100644 --- a/.github/ISSUE_TEMPLATE/bug_report.yml +++ b/.github/ISSUE_TEMPLATE/bug_report.yml @@ -9,7 +9,7 @@ body: attributes: value: | Thanks for taking the time to fill out this bug report. - Please check the existing issues, [Plutus Docs](https://intersectmbo.github.io/plutus/docs) and [Cardano Stack Exchange](https://cardano.stackexchange.com/) before raising. + Please check the existing issues, [Plutus Docs](https://plutus.cardano.intersectmbo.org/docs) and [Cardano Stack Exchange](https://cardano.stackexchange.com/) before raising. - type: textarea id: summary attributes: diff --git a/.github/ISSUE_TEMPLATE/feature_request.yml b/.github/ISSUE_TEMPLATE/feature_request.yml index 34fce863a59..99c76417c80 100644 --- a/.github/ISSUE_TEMPLATE/feature_request.yml +++ b/.github/ISSUE_TEMPLATE/feature_request.yml @@ -8,7 +8,7 @@ body: attributes: value: | Thanks for taking the time to fill out this feature request. - Please check the existing issues and [Plutus Docs](https://intersectmbo.github.io/plutus/docs) before raising. + Please check the existing issues and [Plutus Docs](https://plutus.cardano.intersectmbo.org/docs) before raising. - type: textarea id: description attributes: diff --git a/.github/actions/linkchecker/action.yml b/.github/actions/linkchecker/action.yml deleted file mode 100644 index be894c3e495..00000000000 --- a/.github/actions/linkchecker/action.yml +++ /dev/null @@ -1,81 +0,0 @@ -name: Run Linkchecker - -description: | - Run linkchecker on a URL or a list of files. - This only checks external links. - -inputs: - target-url: - default: "" - description: | - Target url to check for external broken links. - Either this or target-url must be non-empty, not both. - - target-files: - default: "" - description: | - String of space-separated target filepath patterns. - Each pattern will be fed to find using the -name directive. - URLs beginning with "https?" will be regex-matched and extracted from each file. - Either this or target-url must be non-empty, not both. - - ignore-urls: - default: "" - description: | - String of space-separated URL patterns to ignore. - Each URL is fed to linkchecker using the --ignore-url option. - -runs: - using: "composite" - steps: - - name: Check Valid Inputs - if: ${{ inputs.target-url == "" && inputs.target-files == "" || inputs.target-url != "" && inputs.target-files != ""}} - run: - echo "Provide a value for either target-url xor target-files." - exit 1 - - - name: Checkout Repo - if: ${{ inputs.target-url != "" }} - uses: actions/checkout@main - - - name: Check URL - if: ${{ inputs.target-url != "" }} - run: | - linkchecker - echo "Collecting --ignore-url options" - IGNORE_URL_OPTIONS=() - for failure in "${BROKEN_LINKS[@]}"; do - url="${failure##* }" - IGNORE_URL_OPTIONS+=("--ignore-url=${url}") - done - -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}" - - - - name: Check Files - if: ${{ inputs.target-files != "" }} - run: | - 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}" \ No newline at end of file diff --git a/.github/workflows/broken-links.yml b/.github/workflows/broken-links.yml index 7ef2bf44fa9..536a8249a2d 100644 --- a/.github/workflows/broken-links.yml +++ b/.github/workflows/broken-links.yml @@ -1,32 +1,16 @@ -# This job checks for broken links in the various places: -# - The live haddock site -# - The live metatheory site -# - The live docusaurus site -# - Anchors and URLs in various files in the repo +# This job checks for broken links in various files in the repo. 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 + push: + branches: + master jobs: - repo-files: - name: Repo Files + check: + name: Check runs-on: [plutus-shared, self-hosted] steps: - name: Checkout @@ -36,19 +20,5 @@ jobs: run: | nix develop --no-warn-dirty --accept-flake-config --command ./scripts/check-broken-links.sh - - haddock-site: - name: Haddock Site - runs-on: [plutus-shared, self-hosted] - steps: - - name: Checkout - uses: actions/checkout@main - - - name: Run Linkchecker - env: - IGNORE_URLS: - run: | - nix develop --no-warn-dirty --accept-flake-config --command ./scripts/check-broken-links.sh - diff --git a/.github/workflows/docusaurus-site.yml b/.github/workflows/docusaurus-site.yml index eaca8024536..b162559bef4 100644 --- a/.github/workflows/docusaurus-site.yml +++ b/.github/workflows/docusaurus-site.yml @@ -1,5 +1,5 @@ # This workflow builds and publishes the Docusaurus site to: -# https://intersectmbo.github.io/plutus/docs +# https://plutus.cardano.intersectmbo.org/docs name: "🦕 Docusaurus Site" @@ -31,4 +31,13 @@ jobs: folder: doc/docusaurus/build target-folder: docs single-commit: true - + + - name: Check Broken Links + run: | + URL="https://plutus.cardano.intersectmbo.org/docs" + linkchecker --no-status --no-warnings --check-extern --output failures "${URL}" + if [ $? -ne 0 ]; then + echo "${URL}" has broken links, see output above" + exit 1 + fi + \ No newline at end of file diff --git a/.github/workflows/haddock-site.yml b/.github/workflows/haddock-site.yml index 0293a912779..e335d607246 100644 --- a/.github/workflows/haddock-site.yml +++ b/.github/workflows/haddock-site.yml @@ -1,9 +1,9 @@ # This workflow builds and publishes the Haddock site to: -# https://intersectmbo.github.io/plutus/haddock/$version +# https://plutus.cardano.intersectmbo.org/haddock/$version # And optionally to: -# https://intersectmbo.github.io/plutus/haddock/latest +# https://plutus.cardano.intersectmbo.org/haddock/latest # On push to master, this workflows publishes to: -# https://intersectmbo.github.io/plutus/haddock/master +# https://plutus.cardano.intersectmbo.org/haddock/master name: "📜 Haddock Site" @@ -25,14 +25,14 @@ on: destination: description: | The $destination folder, e.g. when "1.29.0.0" the haddock will be deploy to: - https://intersectmbo.github.io/plutus/haddock/1.29.0.0 + https://plutus.cardano.intersectmbo.org/haddock/1.29.0.0 required: true type: string latest: description: | If true, then the haddock site will also be deploy to: - https://intersectmbo.github.io/plutus/haddock/latest. + https://plutus.cardano.intersectmbo.org/haddock/latest. You want to leave this to true unless you are deploying old versions or back-porting. type: boolean required: true @@ -74,4 +74,13 @@ jobs: with: folder: _haddock target-folder: haddock/latest - single-commit: true \ No newline at end of file + single-commit: true + + - name: Check Broken Links + run: | + URL="https://plutus.cardano.intersectmbo.org/haddock/${{ inputs.destination || github.ref_name }}" + linkchecker --no-status --no-warnings --check-extern --output failures "${URL}" + if [ $? -ne 0 ]; then + echo "${URL}" has broken links, see output above" + exit 1 + fi \ No newline at end of file diff --git a/.github/workflows/longitudinal-benchmark.yml b/.github/workflows/longitudinal-benchmark.yml index 87e7b9ae867..0c1eec0aaf0 100644 --- a/.github/workflows/longitudinal-benchmark.yml +++ b/.github/workflows/longitudinal-benchmark.yml @@ -2,8 +2,8 @@ # It will collect and aggreate the benchmark output, format it and feed it to the # github-action-benchmark action. # -# The benchmark charts are live at https://intersectmbo.github.io/plutus/dev/bench -# The benchmark data is available at https://intersectmbo.github.io/plutus/dev/bench/data.js +# The benchmark charts are live at https://plutus.cardano.intersectmbo.org/dev/bench +# The benchmark data is available at https://plutus.cardano.intersectmbo.org/dev/bench/data.js # # This is a performance regression check that is run on every push master. diff --git a/.github/workflows/metatheory-site.yml b/.github/workflows/metatheory-site.yml index 2508fbc8207..9e3d8a71db9 100644 --- a/.github/workflows/metatheory-site.yml +++ b/.github/workflows/metatheory-site.yml @@ -1,9 +1,9 @@ # This workflow builds and publishes the metatheory site to: -# https://intersectmbo.github.io/plutus/metatheory/$version +# https://plutus.cardano.intersectmbo.org/metatheory/$version # And optionally to: -# https://intersectmbo.github.io/plutus/metatheory/latest +# https://plutus.cardano.intersectmbo.org/metatheory/latest # On push to master, this workflows publishes to: -# https://intersectmbo.github.io/plutus/metatheory/master +# https://plutus.cardano.intersectmbo.org/metatheory/master name: "🔮 Metatheory Site" @@ -25,14 +25,14 @@ on: destination: description: | The $destination folder, e.g. when "1.29.0.0" the metatheory will be deploy to: - https://intersectmbo.github.io/plutus/metatheory/1.29.0.0 + https://plutus.cardano.intersectmbo.org/metatheory/1.29.0.0 required: true type: string latest: description: | If true, then the metatheory site will also be deploy to: - https://intersectmbo.github.io/plutus/metatheory/latest. + https://plutus.cardano.intersectmbo.org/metatheory/latest. You want to leave this to true unless you are deploying old versions or back-porting. type: boolean required: true @@ -73,3 +73,11 @@ jobs: target-folder: metatheory/latest single-commit: true + - name: Check Broken Links + run: | + URL="https://plutus.cardano.intersectmbo.org/metatheory/${{ inputs.destination || github.ref_name }}" + linkchecker --no-status --no-warnings --check-extern --output failures "${URL}" + if [ $? -ne 0 ]; then + echo "${URL}" has broken links, see output above" + exit 1 + fi \ No newline at end of file diff --git a/.github/workflows/papers-and-specs.yml b/.github/workflows/papers-and-specs.yml index 53b96b37b43..8f5a49791fa 100644 --- a/.github/workflows/papers-and-specs.yml +++ b/.github/workflows/papers-and-specs.yml @@ -1,5 +1,5 @@ # This job builds various papers and deploys them to: -# https://intersectmbo.github.io/plutus/resources +# https://plutus.cardano.intersectmbo.org/resources name: "📝 Papers & Specs" diff --git a/README.adoc b/README.adoc index 2f244db47b9..8c0cedc5ac9 100644 --- a/README.adoc +++ b/README.adoc @@ -42,11 +42,11 @@ After setting it up you should just be able to depend on the `plutus` packages a === User documentation -The main documentation is located https://intersectmbo.github.io/plutus/docs/[here]. +The main documentation is located https://plutus.cardano.intersectmbo.org/docs/[here]. -The haddock documentation is located https://intersectmbo.github.io/plutus/haddock/latest[here]. +The haddock documentation is located https://plutus.cardano.intersectmbo.org/haddock/latest[here]. -The documentation for the metatheory can be found https://intersectmbo.github.io/plutus/metatheory/latest[here]. +The documentation for the metatheory can be found https://plutus.cardano.intersectmbo.org/metatheory[here]. === Talks @@ -55,17 +55,17 @@ The documentation for the metatheory can be found https://intersectmbo.github.io === Specifications and design -- 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. +- https://plutus.cardano.intersectmbo.org/resources/plutus-report.pdf[Plutus Technical Report (draft)]: a technical report and design document for the project. +- https://plutus.cardano.intersectmbo.org/resources/plutus-core-spec.pdf[Plutus Core Specification]: the formal specification of the core language. +- https://plutus.cardano.intersectmbo.org/resources/extended-utxo-spec.pdf[Extended UTXO Model]: a design document for the core changes to the Cardano ledger. === Academic papers -- 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://plutus.cardano.intersectmbo.org/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://plutus.cardano.intersectmbo.org/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://plutus.cardano.intersectmbo.org/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://plutus.cardano.intersectmbo.org/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://plutus.cardano.intersectmbo.org/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 diff --git a/doc/docusaurus/README.md b/doc/docusaurus/README.md index 950f424e650..fa454557233 100644 --- a/doc/docusaurus/README.md +++ b/doc/docusaurus/README.md @@ -19,4 +19,4 @@ yarn start # for live development on localhost Go to the [docusaurus-site.yml](https://github.com/IntersectMBO/plutus/actions/workflows/docusaurus-site.yml) workflow and click `Run workflow` on the right. -This will build and publish the website to [GitHub pages](https://intersectmbo.github.io/plutus/docs). \ No newline at end of file +This will build and publish the website to [GitHub pages](https://plutus.cardano.intersectmbo.org/plutus/docs). \ No newline at end of file diff --git a/doc/docusaurus/docs/essential-concepts/plutus-foundation.md b/doc/docusaurus/docs/essential-concepts/plutus-foundation.md index b53ec64fffa..11661ff9e45 100644 --- a/doc/docusaurus/docs/essential-concepts/plutus-foundation.md +++ b/doc/docusaurus/docs/essential-concepts/plutus-foundation.md @@ -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://intersectmbo.github.io/plutus/resources/plutus-report.pdf). +The design is discussed in the [technical report](https://plutus.cardano.intersectmbo.org/plutus/resources/plutus-report.pdf). diff --git a/doc/docusaurus/docs/essential-concepts/plutus-platform.mdx b/doc/docusaurus/docs/essential-concepts/plutus-platform.mdx index 83591138697..e72ac1d24d3 100644 --- a/doc/docusaurus/docs/essential-concepts/plutus-platform.mdx +++ b/doc/docusaurus/docs/essential-concepts/plutus-platform.mdx @@ -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://intersectmbo.github.io/plutus/resources/plutus-report.pdf). +- The design of the platform is discussed in the [Plutus technical report](https://plutus.cardano.intersectmbo.org/plutus/resources/plutus-report.pdf). diff --git a/doc/docusaurus/docs/index.md b/doc/docusaurus/docs/index.md index a605d4b7093..0512a107681 100644 --- a/doc/docusaurus/docs/index.md +++ b/doc/docusaurus/docs/index.md @@ -17,7 +17,7 @@ All of these elements are used in combination to write Plutus Core scripts that To develop and deploy a smart contract, you also need off-chain code for building transactions, submitting transactions, deploying smart contracts, querying for available UTXOs on the chain, and so on. You may also want a front-end interface for your smart contract for a better user experience. -Plutus allows all programming to be done from a [single Haskell library](https://intersectmbo.github.io/plutus/haddock/latest). This lets developers build secure applications, forge new assets, and create smart contracts in a predictable, deterministic environment with the highest level of assurance. Furthermore, developers don’t have to run a full Cardano node to test their work. +Plutus allows all programming to be done from a [single Haskell library](https://plutus.cardano.intersectmbo.org/plutus/haddock/latest). This lets developers build secure applications, forge new assets, and create smart contracts in a predictable, deterministic environment with the highest level of assurance. Furthemore, developers don’t have to run a full Cardano node to test their work. With Plutus you can: @@ -38,7 +38,7 @@ See, for example: - the [Cardano ledger specification](https://github.com/IntersectMBO/cardano-ledger#cardano-ledger) - the [Plutus Core specification](https://github.com/IntersectMBO/plutus#specifications-and-design) -- the [public Plutus code libraries](https://intersectmbo.github.io/plutus/haddock/latest) generated using Haddock. +- the [public Plutus code libraries](https://plutus.cardano.intersectmbo.org/plutus/haddock/latest) generated using Haddock. ## The Plutus repository @@ -46,7 +46,7 @@ The [Plutus repository](https://github.com/IntersectMBO/plutus) includes: * the implementation, specification, and mechanized metatheory of Plutus Core * the Plutus Tx compiler -* the combined documentation, generated using Haddock, for all the [public Plutus code libraries](https://intersectmbo.github.io/plutus/haddock/latest), such as `PlutusTx.List`, enabling developers to write Haskell code that can be compiled to Plutus Core. +* the combined documentation, generated using Haddock, for all the [public Plutus code libraries](https://plutus.cardano.intersectmbo.org/plutus/haddock/latest), such as `PlutusTx.List`, enabling developers to write Haskell code that can be compiled to Plutus Core. ## Educational resources diff --git a/doc/docusaurus/docs/reference/haddock-documentation.md b/doc/docusaurus/docs/reference/haddock-documentation.md index c84d9345092..c9d9fb8d5d5 100644 --- a/doc/docusaurus/docs/reference/haddock-documentation.md +++ b/doc/docusaurus/docs/reference/haddock-documentation.md @@ -6,12 +6,12 @@ sidebar_position: 3 ## Public Plutus code libraries -The documentation generated by Haddock provides a comprehehsive reference for the [public Plutus code libraries](https://intersectmbo.github.io/plutus/haddock/latest), an essential resource for developers working with Haskell and Plutus Core. +The documentation generated by Haddock provides a comprehehsive reference for the [public Plutus code libraries](https://plutus.cardano.intersectmbo.org/plutus/haddock/latest), an essential resource for developers working with Haskell and Plutus Core. ### Highlighted modules Highlighted modules in the documentation include the following: -- [PlutusTx](https://intersectmbo.github.io/plutus/haddock/latest/plutus-tx/PlutusTx.html): compiling Haskell to PLC (Plutus Core; on-chain code) -- [PlutusTx.Prelude](https://intersectmbo.github.io/plutus/haddock/latest/plutus-tx/PlutusTx-Prelude.html): Haskell prelude replacement compatible with PLC -- [PlutusCore](https://intersectmbo.github.io/plutus/haddock/latest/plutus-core/PlutusCore.html): programming language in which scripts on the Cardano blockchain are written -- [UntypedPlutusCore](https://intersectmbo.github.io/plutus/haddock/latest/plutus-core/UntypedPlutusCore.html): on-chain Plutus code. +- [PlutusTx](https://plutus.cardano.intersectmbo.org/plutus/haddock/latest/plutus-tx/PlutusTx.html): compiling Haskell to PLC (Plutus Core; on-chain code) +- [PlutusTx.Prelude](https://plutus.cardano.intersectmbo.org/plutus/haddock/latest/plutus-tx/PlutusTx-Prelude.html): Haskell prelude replacement compatible with PLC +- [PlutusCore](https://plutus.cardano.intersectmbo.org/plutus/haddock/latest/plutus-core/PlutusCore.html): programming language in which scripts on the Cardano blockchain are written +- [UntypedPlutusCore](https://plutus.cardano.intersectmbo.org/plutus/haddock/latest/plutus-core/UntypedPlutusCore.html): on-chain Plutus code. diff --git a/doc/docusaurus/docusaurus.config.ts b/doc/docusaurus/docusaurus.config.ts index 2f1b3ee1bbf..8d0d6cedb18 100644 --- a/doc/docusaurus/docusaurus.config.ts +++ b/doc/docusaurus/docusaurus.config.ts @@ -8,14 +8,11 @@ const config: Config = { favicon: "img/favicon.ico", // Set the production url of your site here - url: "https://intersectmbo.github.io", + // This will end be used inside meta and link tags in each page's . + url: "https://plutus.cardano.intersectmbo.org", // Set the // pathname under which your site is served // For GitHub pages deployment, it is often '//' - // WARNING: normally this would be /plutus/docs/, because - // https://intersectmbo.github.io is a GitHub Pages URL. - // However we setup a redirect from intersectmbo.github.io/plutus - // to plutus.cardano.intersectmbo.org, so /docs/ is used here instead. baseUrl: "/docs/", // GitHub pages deployment config. diff --git a/doc/plutus-core-spec/README.md b/doc/plutus-core-spec/README.md index 85ec0985cc3..d602b09a80b 100644 --- a/doc/plutus-core-spec/README.md +++ b/doc/plutus-core-spec/README.md @@ -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://intersectmbo.github.io/plutus/resources/plutus-core-spec.pdf) +[here](https://plutus.cardano.intersectmbo.org/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. diff --git a/doc/read-the-docs-site/README.md b/doc/read-the-docs-site/README.md index 7d537985e9b..fedea23c0f8 100644 --- a/doc/read-the-docs-site/README.md +++ b/doc/read-the-docs-site/README.md @@ -6,11 +6,11 @@ https://plutus.readthedocs.io ``` Is now permanently redirecting to: ``` -https://intersectmbo.github.io/plutus/docs +https://plutus.cardano.intersectmbo.org/docs ``` Using the [Exact Redirect](https://readthedocs.org/dashboard/plutus/redirects/): ``` -/* -> https://intersectmbo.github.io/plutus/docs +/* -> https://plutus.cardano.intersectmbo.org/docs ``` And the [GitHub Webhook](https://readthedocs.org/dashboard/plutus/webhooks/) has been deleted. diff --git a/plutus-core/docs/BuiltinsOverview.md b/plutus-core/docs/BuiltinsOverview.md index 5a13d7d33b2..fc213b2370e 100644 --- a/plutus-core/docs/BuiltinsOverview.md +++ b/plutus-core/docs/BuiltinsOverview.md @@ -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://intersectmbo.github.io/plutus/resources/plutus-core-spec.pdf#page=8). +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://plutus.cardano.intersectmbo.org/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: diff --git a/plutus-metatheory/README.md b/plutus-metatheory/README.md index 441925d2b54..5bc3d1bff22 100644 --- a/plutus-metatheory/README.md +++ b/plutus-metatheory/README.md @@ -100,7 +100,7 @@ $ jekyll build -s html -d html/_site ## Detailed Description -See the [table of contents](https://input-output-hk.github.io/plutus-metatheory/) for an explanation of the structure of the formalisation and links to the code. +See the [table of contents](https://plutus.cardano.intersectmbo.org/metatheory/) for an explanation of the structure of the formalisation and links to the code. **The below information is deprecated and is in the process of being replaced by the table of contents document.** @@ -119,51 +119,51 @@ Then, two different implementations of the term language: ## Types Types are defined in the -[Type](https://input-output-hk.github.io/plutus-metatheory/Type.html) +[Type](https://plutus.cardano.intersectmbo.org/metatheory/Type.html) module. They are intrinsically kinded so it is impossible to apply a type operator to arguments of the wrong kind. The type module is further subdivided into submodules: -1. [Type.RenamingSubstitution](https://input-output-hk.github.io/plutus-metatheory/Type.RenamingSubstitution.html) +1. [Type.RenamingSubstitution](https://plutus.cardano.intersectmbo.org/metatheory/Type.RenamingSubstitution.html) contains the operations of renaming and substitution for types and their proofs of correctness. These are necessary to, for example, define the beta rule for types in the equational theory and reduction relation (described below). -2. [Type.Equality](https://input-output-hk.github.io/plutus-metatheory/Type.Equality.html) contains the beta-equational +2. [Type.Equality](https://plutus.cardano.intersectmbo.org/metatheory/Type.Equality.html) contains the beta-equational theory of types. This is essentially a specification for the computational behaviour of types. -3. [Type.Reduction](https://input-output-hk.github.io/plutus-metatheory/Type.Reduction.html) contains the small step +3. [Type.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Type.Reduction.html) contains the small step reduction relation, the progress/preservation results for types, and an evaluator for types. This result is not used later in the development but is in the spec. -4. [Type.BetaNormal](https://input-output-hk.github.io/plutus-metatheory/Type.BetaNormal.html) contains beta normal forms +4. [Type.BetaNormal](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNormal.html) contains beta normal forms for types as a separate syntax. Beta normal forms contain no beta-redexes and guaranteed not to compute any further. -5. [Type.BetaNBE](https://input-output-hk.github.io/plutus-metatheory/Type.BetaNBE.html) contains a beta normaliser for +5. [Type.BetaNBE](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.html) contains a beta normaliser for types, it is defined in the style of "normalization-by-evaluation" (NBE) and is guaranteed to terminate. Further submodules define the correctness proofs for the normalizer and associated operations. - 1. [Type.BetaNBE.Soundness](https://input-output-hk.github.io/plutus-metatheory/Type.BetaNBE.Soundness.html) contains a + 1. [Type.BetaNBE.Soundness](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.Soundness.html) contains a proof that normalizer preserves the meaning of the types. Formally it states that if we normalize a type then the resultant normal form is equal (in the equational theory) to the type we started with. - 2. [Type.BetaNBE.Completeness](https://input-output-hk.github.io/plutus-metatheory/Type.BetaNBE.Completeness.html) + 2. [Type.BetaNBE.Completeness](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.Completeness.html) contains a proof that the if we were to normalize two types that are equal in the equation theory then we will end up with identical normal forms. - 3. [Type.BetaNBE.Stability](https://input-output-hk.github.io/plutus-metatheory/Type.BetaNBE.Stability.html) contains a + 3. [Type.BetaNBE.Stability](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.Stability.html) contains a proof that normalization will preserve syntactic structure of terms already in normal form. - 4. [Type.BetaNBE.RenamingSubsitution](https://input-output-hk.github.io/plutus-metatheory/Type.BetaNBE.RenamingSubstitution.html) + 4. [Type.BetaNBE.RenamingSubsitution](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.RenamingSubstitution.html) contains a version of substitution that works on normal forms and ensures that the result is in normal form. This works by embedding normal forms back into syntax, performing a syntactic substitution and @@ -183,18 +183,18 @@ level programs computing. There are builtin types of integers and bytestrings. -1. [Builtin.Constant.Type](https://input-output-hk.github.io/plutus-metatheory/Builtin.Constant.Type.html) +1. [Builtin.Constant.Type](https://plutus.cardano.intersectmbo.org/metatheory/Builtin.Constant.Type.html) contains the enumeration of the type constants. -2. [Builtin.Constant.Term](https://input-output-hk.github.io/plutus-metatheory/Builtin.Constant.Term.html) +2. [Builtin.Constant.Term](https://plutus.cardano.intersectmbo.org/metatheory/Builtin.Constant.Term.html) contains the enumeration of the term constants at the bottom. -3. [Builtin.Signature](https://input-output-hk.github.io/plutus-metatheory/Builtin.Signature.html) +3. [Builtin.Signature](https://plutus.cardano.intersectmbo.org/metatheory/Builtin.Signature.html) contains the list of builtin operations and their type signatures. In the specification this information is contained in the large builtin table. The rest of the Builtin machinery: telescopes, and the semantics of builtins are contained in -[Declarative.Term.Reduction](https://input-output-hk.github.io/plutus-metatheory/Declarative.Term.Reduction.html). +[Declarative.Term.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.Reduction.html). ## Terms indexed by syntactic types @@ -214,32 +214,32 @@ constructor. They fail if they encounter it. Nevertheless this is sufficient to handle examples which do not require computing the types before applying beta-reductions. Such as Church/Scott Numerals. -1. The [Declarative.Term](https://input-output-hk.github.io/plutus-metatheory/Declarative.Term.html) +1. The [Declarative.Term](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.html) module contains the definition of terms. This module has two further submodules: - 1. [Declarative.Term.RenamingSubstitution](https://input-output-hk.github.io/plutus-metatheory/Declarative.Term.RenamingSubstitution.html) + 1. [Declarative.Term.RenamingSubstitution](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.RenamingSubstitution.html) contains the definitions of substitution for terms that is necessary to specify the beta-rules in the reduction relation. This definition and those it depends on, in turn, depend on the definitions and correctness proofs of the corresponding type level operations. - 2. [Declarative.Term.Reduction](https://input-output-hk.github.io/plutus-metatheory/Declarative.Term.Reduction.html) + 2. [Declarative.Term.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.Reduction.html) This file contains the reduction relation for terms (also known as the small step operational semantics) and the progress proof. Preservation is inherent. Note: this version of progress doesn't handle type conversions in terms. -2. [Declarative.Evaluation](https://input-output-hk.github.io/plutus-metatheory/Declarative.Evaluation.html) +2. [Declarative.Evaluation](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Evaluation.html) contains the evaluator the terms. It takes a *gas* argument which is the number of steps of reduction that are allowed. It returns both a result and trace of reduction steps or *out of gas*. Note: this version of evaluation doesn't handle type conversions in terms. -3. [Declarative.Examples](https://input-output-hk.github.io/plutus-metatheory/Declarative.Examples.html) +3. [Declarative.Examples](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Examples.html) contains some examples of Church and Scott Numerals. Currently it is very memory intensive to type check this file and/or run examples. -4. [Erasure](https://input-output-hk.github.io/plutus-metatheory/Declarative.Erasure.html) +4. [Erasure](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Erasure.html) ## Terms indexed by normal types @@ -252,10 +252,10 @@ deal with conversions in the syntax. This allows us to define progress, preservation, and evaluation for the full language of System F omega with iso-recursive types and sized integers and bytestrings. -1. The [Algorithmic.Term](https://input-output-hk.github.io/plutus-metatheory/Algorithmic.Term.html) +1. The [Algorithmic.Term](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Term.html) module contains the definition of terms. This module has two further submodules: - 1. [Algorithmic.Term.RenamingSubstitution](https://input-output-hk.github.io/plutus-metatheory/Algorithmic.Term.RenamingSubstitution.html) + 1. [Algorithmic.Term.RenamingSubstitution](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Term.RenamingSubstitution.html) contains the definitions of substitution for terms that is necessary to specify the beta-rules in the reduction relation. This definition and those it depends on, in turn, @@ -264,32 +264,32 @@ module contains the definition of terms. This module has two further submodules: includes depeneding on the correctness proof of the beta normalizer for types. - 2. [Algorithmic.Term.Reduction](https://input-output-hk.github.io/plutus-metatheory/Algorithmic.Term.Reduction.html) + 2. [Algorithmic.Term.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Term.Reduction.html) This file contains the reduction relation for terms (also known as the small step operational semantics) and the progress proof. Preservation is, again, inherent. -2. [Algorithmic.Evaluation](https://input-output-hk.github.io/plutus-metatheory/Algorithmic.Evaluation.html) +2. [Algorithmic.Evaluation](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Evaluation.html) contains the evaluator the terms. It takes a *gas* argument which is the number of steps of reduction that are allowed. It returns both a result and trace of reduction steps or *out of gas*. -3. [Algorithmic.Examples](https://input-output-hk.github.io/plutus-metatheory/Algorithmic.Examples.html) +3. [Algorithmic.Examples](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Examples.html) contains some examples of Church and Scott Numerals. Currently it is very memory intensive to type check this file and/or run examples. We also need to show that the algorithmic version of the type system is sound and complete. -4. [Algorithmic.Soundness](https://input-output-hk.github.io/plutus-metatheory/Algorithmic.Soundness.html) +4. [Algorithmic.Soundness](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Soundness.html) Programmatically this corresponds to taking a term with normal type and converting it back to a term with a syntactic type. This introduces conversions into the term anywhere there a substitution occurs in a type. -4. [Algorithmic.Completeness](https://input-output-hk.github.io/plutus-metatheory/Algorithmic.Completeness.html) +4. [Algorithmic.Completeness](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Completeness.html) -5. [Erasure](https://input-output-hk.github.io/plutus-metatheory/Algorithmic.Erasure.html) contains erasure to untyped lambda calculus. +5. [Erasure](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Erasure.html) contains erasure to untyped lambda calculus. Programmatically this correponds to taking a term with a syntactic type that may contain conversions and normalising its type by @@ -297,37 +297,37 @@ collapsing all the conversions. # Extrinsically typed version -1. [Syntax](https://input-output-hk.github.io/plutus-metatheory/Scoped.html) +1. [Syntax](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.html) contains the intrinsically scoped but extrinsically typed terms, and intrinsically scoped but extrinscically kinded types. 2. [Renaming and -Substitution](https://input-output-hk.github.io/plutus-metatheory/Scoped.RenamingSubstitution.html) +Substitution](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.RenamingSubstitution.html) contains the operations of renaming and substitution for extrinsically typed terms, and extrinsically kinded types. -3. [Reduction](https://input-output-hk.github.io/plutus-metatheory/Scoped.Reduction.html) contains the reduction rules, progress and evaluation. +3. [Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Reduction.html) contains the reduction rules, progress and evaluation. -4. [Extrication](https://input-output-hk.github.io/plutus-metatheory/Scoped.Extrication.html) +4. [Extrication](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Extrication.html) contains the operations to convert from intrinsically typed to extrinscally typed syntax. -5. [Erasure](https://input-output-hk.github.io/plutus-metatheory/Scoped.Erasure.html) +5. [Erasure](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Erasure.html) contains operations to erase the types yielding untyped terms. 1. [Renaming and - Substitution](https://input-output-hk.github.io/plutus-metatheory/Scoped.Erasure.RenamingSubstitution.html) + Substitution](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Erasure.RenamingSubstitution.html) contains operations to erase the types in extrinsic renamings and substitutions yielding untyped renamings and substitutions. # Untyped version -1. [Syntax](https://input-output-hk.github.io/plutus-metatheory/Untyped.html) +1. [Syntax](https://plutus.cardano.intersectmbo.org/metatheory/Untyped.html) contains intrinsically scoped but untyped lambda calculus extended with builtins. 2. [Renaming and -Substitution](https://input-output-hk.github.io/plutus-metatheory/Untyped.RenamingSubstitution.html) +Substitution](https://plutus.cardano.intersectmbo.org/metatheory/Untyped.RenamingSubstitution.html) contains operations for untyped renaming and substitution. -3. [Reduction](https://input-output-hk.github.io/plutus-metatheory/Untyped.Reduction.html) contains the untyped reduction rules. +3. [Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Untyped.Reduction.html) contains the untyped reduction rules. diff --git a/plutus-metatheory/src/Builtin.lagda.md b/plutus-metatheory/src/Builtin.lagda.md index ac170bb5e2c..6662d72c408 100644 --- a/plutus-metatheory/src/Builtin.lagda.md +++ b/plutus-metatheory/src/Builtin.lagda.md @@ -201,7 +201,7 @@ and constructs a signature sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ - ``` +``` ArgSet : Set ArgSet = Σ (ℕ × ℕ) (λ { (n⋆ ,, n♯) → Args n⋆ n♯}) @@ -219,11 +219,11 @@ sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ infix 8 _]⟶_ _]⟶_ : (p : ArgSet) → ArgTy p → Sig _]⟶_ ((n⋆ ,, n♯) ,, as) res = sig n⋆ n♯ as res - ``` +``` The signature of each builtin - ``` +``` signature : Builtin → Sig signature addInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑ signature subtractInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑ diff --git a/plutus-metatheory/src/Type/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Type/RenamingSubstitution.lagda.md index daa0616be68..ae31219c638 100644 --- a/plutus-metatheory/src/Type/RenamingSubstitution.lagda.md +++ b/plutus-metatheory/src/Type/RenamingSubstitution.lagda.md @@ -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://intersectmbo.github.io/plutus/resources/plutus-core-spec.pdf#page=8) ). +called `lift⋆` in the [paper](https://plutus.cardano.intersectmbo.org/resources/plutus-core-spec.pdf#page=8) ). ``` ext : Ren Φ Ψ @@ -252,7 +252,7 @@ variable σ σ' : Sub Φ Ψ ``` -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) ). +Extending a type substitution — used when going under a binder. (This is called `lifts` in the [paper](https://plutus.cardano.intersectmbo.org/resources/plutus-core-spec.pdf#page=8) ). ``` exts : Sub Φ Ψ diff --git a/scripts/check-broken-links.sh b/scripts/check-broken-links.sh index 55787ef2ad9..3dd731f0866 100755 --- a/scripts/check-broken-links.sh +++ b/scripts/check-broken-links.sh @@ -1,24 +1,27 @@ 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 + .github/{ISSUE_TEMPLATE/*,*.md,*.yml} + **/{LICENSE,NOTICE,README.md,TRIAGE.md} + CODE_OF_CONDUCT.md + *.adoc +) + +IGNORE_URLS=( + --ignore-url https://img.shields.io/matrix/plutus-core%3Amatrix.org # For some reason linkchecker fails to check this URL though it is valid ) FAILED=0 -for file in "${TARGETS[@]}"; do +grep_links() { + grep -oE "\b(https?://|www\.)[^\[\(\)\"]+\b" "$1" +} + +check_links() { + linkchecker --no-status --no-warnings --recursion-level 0 --output failures --check-extern "${IGNORE_URLS[@]}" --stdin +} + +for file in $(find "${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 + grep_links "${file}" | check_links if [ $? -ne 0 ]; then echo "${file} has broken links, see output above" FAILED=1 diff --git a/scripts/combined-haddock.sh b/scripts/combined-haddock.sh index 6cfed90f4de..a06db53c75e 100755 --- a/scripts/combined-haddock.sh +++ b/scripts/combined-haddock.sh @@ -222,7 +222,7 @@ fi echo "Running linkchecker" -time linkchecker "${OUTPUT_DIR}/index.html" \ +time linkchecker --no-status "${OUTPUT_DIR}/index.html" \ --check-extern \ --no-warnings \ --output failures \ From 9587a9fb582aac4a2219befd239abb68d951f269 Mon Sep 17 00:00:00 2001 From: zeme Date: Mon, 8 Jul 2024 09:28:20 +0200 Subject: [PATCH 3/8] Wip --- .github/workflows/metatheory-site.yml | 46 ++------------------------- doc/docusaurus/docusaurus.config.ts | 1 - 2 files changed, 3 insertions(+), 44 deletions(-) diff --git a/.github/workflows/metatheory-site.yml b/.github/workflows/metatheory-site.yml index 9e3d8a71db9..7b848cac4fd 100644 --- a/.github/workflows/metatheory-site.yml +++ b/.github/workflows/metatheory-site.yml @@ -1,9 +1,5 @@ # This workflow builds and publishes the metatheory site to: -# https://plutus.cardano.intersectmbo.org/metatheory/$version -# And optionally to: -# https://plutus.cardano.intersectmbo.org/metatheory/latest -# On push to master, this workflows publishes to: -# https://plutus.cardano.intersectmbo.org/metatheory/master +# https://plutus.cardano.intersectmbo.org/metatheory name: "🔮 Metatheory Site" @@ -11,32 +7,6 @@ on: push: branches: - master - - workflow_dispatch: - inputs: - ref: - description: | - The $ref to build off of, e.g. "1.29.0.0", "master", or any other valid git ref. - When making a release, this is usually the version tag, e.g. "1.29.0.0", and will be - equal to the $destination input below. When back-porting this could be a commit sha instead. - required: true - type: string - - destination: - description: | - The $destination folder, e.g. when "1.29.0.0" the metatheory will be deploy to: - https://plutus.cardano.intersectmbo.org/metatheory/1.29.0.0 - required: true - type: string - - latest: - description: | - If true, then the metatheory site will also be deploy to: - https://plutus.cardano.intersectmbo.org/metatheory/latest. - You want to leave this to true unless you are deploying old versions or back-porting. - type: boolean - required: true - default: true jobs: deploy: @@ -49,8 +19,6 @@ jobs: steps: - name: Checkout uses: actions/checkout@main - with: - ref: ${{ inputs.ref || github.ref_name }} - name: Build Site run: | @@ -62,20 +30,12 @@ jobs: uses: JamesIves/github-pages-deploy-action@v4.6.3 with: folder: _site - target-folder: metatheory/${{ inputs.destination || github.ref_name }} - single-commit: true - - - name: Deploy Latest - if: ${{ inputs.latest == true }} - uses: JamesIves/github-pages-deploy-action@v4.6.3 - with: - folder: _site - target-folder: metatheory/latest + target-folder: metatheory single-commit: true - name: Check Broken Links run: | - URL="https://plutus.cardano.intersectmbo.org/metatheory/${{ inputs.destination || github.ref_name }}" + URL="https://plutus.cardano.intersectmbo.org/metatheory" linkchecker --no-status --no-warnings --check-extern --output failures "${URL}" if [ $? -ne 0 ]; then echo "${URL}" has broken links, see output above" diff --git a/doc/docusaurus/docusaurus.config.ts b/doc/docusaurus/docusaurus.config.ts index 8d0d6cedb18..20fd04c9174 100644 --- a/doc/docusaurus/docusaurus.config.ts +++ b/doc/docusaurus/docusaurus.config.ts @@ -8,7 +8,6 @@ const config: Config = { favicon: "img/favicon.ico", // Set the production url of your site here - // This will end be used inside meta and link tags in each page's . url: "https://plutus.cardano.intersectmbo.org", // Set the // pathname under which your site is served From 5878d7202ca2eb4659b817e02173fd6b9308ee9e Mon Sep 17 00:00:00 2001 From: zeme Date: Mon, 8 Jul 2024 10:00:12 +0200 Subject: [PATCH 4/8] wip --- .github/workflows/docusaurus-site.yml | 5 +- .github/workflows/haddock-site.yml | 278 +++++++++++++++++++++++++- .github/workflows/metatheory-site.yml | 2 +- scripts/check-broken-links.sh | 2 +- scripts/combined-haddock.sh | 3 +- 5 files changed, 283 insertions(+), 7 deletions(-) diff --git a/.github/workflows/docusaurus-site.yml b/.github/workflows/docusaurus-site.yml index b162559bef4..2d02c0e80f8 100644 --- a/.github/workflows/docusaurus-site.yml +++ b/.github/workflows/docusaurus-site.yml @@ -34,8 +34,11 @@ jobs: - name: Check Broken Links run: | + IGNORE_URLS=( + --ignore-url https://plutus.cardano.intersectmbo.org/docs/haddock/.* + ) URL="https://plutus.cardano.intersectmbo.org/docs" - linkchecker --no-status --no-warnings --check-extern --output failures "${URL}" + linkchecker --no-warnings --check-extern --output failures "${URL}" "${IGNORE_URL}" if [ $? -ne 0 ]; then echo "${URL}" has broken links, see output above" exit 1 diff --git a/.github/workflows/haddock-site.yml b/.github/workflows/haddock-site.yml index e335d607246..99dee8f8106 100644 --- a/.github/workflows/haddock-site.yml +++ b/.github/workflows/haddock-site.yml @@ -78,9 +78,283 @@ jobs: - name: Check Broken Links run: | + IGNORE_URLS=( + --ignore-url file:///run/github-runner/plutus-shared/.local/state/cabal/store/.* + --ignore-url https://hackage.haskell.org/package/base-4.18.2.1/docs/Data-Semigroup-Internal.html + --ignore-url https://hackage.haskell.org/package/ghc-9.6.5/docs/-/issues/7100 + --ignore-url https://hackage.haskell.org/package/ghc-boot-th-9.6.5/docs/GHC-ForeignSrcLang-Type.html + --ignore-url https://hackage.haskell.org/package/ghc-boot-th-9.6.5/docs/GHC-LanguageExtensions-Type.html + --ignore-url https://hackage.haskell.org/package/ghc-boot-th-9.6.5/docs/src/GHC.LanguageExtensions.Type.html + --ignore-url .*/plutus-core/... + --ignore-url .*/plutus-core/AlwaysInline + --ignore-url .*/plutus-core/Barbies-Generics-Traversable.html + --ignore-url .*/plutus-core/Barbies-Internal-Containers.html + --ignore-url .*/plutus-core/Barbies-Internal-Trivial.html + --ignore-url .*/plutus-core/Basement-Bits.html + --ignore-url .*/plutus-core/Basement-Nat.html + --ignore-url .*/plutus-core/Basement-Numerical-Subtractive.html + --ignore-url .*/plutus-core/Basement-PrimType.html + --ignore-url .*/plutus-core/Basement-String-Encoding-ASCII7.html + --ignore-url .*/plutus-core/Basement-String-Encoding-ISO_8859_1.html + --ignore-url .*/plutus-core/Basement-String-Encoding-UTF16.html + --ignore-url .*/plutus-core/Basement-String-Encoding-UTF32.html + --ignore-url .*/plutus-core/Cardano-Crypto-DSIGN-Class.html + --ignore-url .*/plutus-core/Cardano-Crypto-DSIGN-EcdsaSecp256k1.html + --ignore-url .*/plutus-core/Cardano-Crypto-DSIGN-Ed25519.html + --ignore-url .*/plutus-core/Cardano-Crypto-DSIGN-SchnorrSecp256k1.html + --ignore-url .*/plutus-core/Cardano-Crypto-Hash-Class.html + --ignore-url .*/plutus-core/Cardano-Crypto-PackedBytes.html + --ignore-url .*/plutus-core/Cardano-Crypto-PinnedSizedBytes.html + --ignore-url .*/plutus-core/Cek-Internal.html + --ignore-url .*/plutus-core/Codec-CBOR-Read.html + --ignore-url .*/plutus-core/Codec-Serialise-Class.html + --ignore-url .*/plutus-core/Control-Applicative-Backwards.html + --ignore-url .*/plutus-core/Control-Applicative-Lift.html + --ignore-url .*/plutus-core/Control-Comonad-Cofree.html + --ignore-url .*/plutus-core/Control-Comonad-Trans-Cofree.html + --ignore-url .*/plutus-core/Control-Composition.html + --ignore-url .*/plutus-core/Control-Lens-At.html + --ignore-url .*/plutus-core/Control-Lens-Cons.html + --ignore-url .*/plutus-core/Control-Lens-Each.html + --ignore-url .*/plutus-core/Control-Lens-Internal-Exception.html + --ignore-url .*/plutus-core/Control-Lens-Internal-Indexed.html + --ignore-url .*/plutus-core/Control-Lens-Internal-Iso.html + --ignore-url .*/plutus-core/Control-Lens-Internal-Prism.html + --ignore-url .*/plutus-core/Control-Lens-Plated.html + --ignore-url .*/plutus-core/Control-Lens-Reified.html + --ignore-url .*/plutus-core/Control-Lens-Wrapped.html + --ignore-url .*/plutus-core/Control-Lens-Zoom.html + --ignore-url .*/plutus-core/Control-Monad-Free-Class.html + --ignore-url .*/plutus-core/Control-Monad-Free.html + --ignore-url .*/plutus-core/Control-Monad-Primitive.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Accum.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Cont.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Except.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Free.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Identity.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Maybe.html + --ignore-url .*/plutus-core/Control-Monad-Trans-RWS-CPS.html + --ignore-url .*/plutus-core/Control-Monad-Trans-RWS-Lazy.html + --ignore-url .*/plutus-core/Control-Monad-Trans-RWS-Strict.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Reader.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Resource-Internal.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Select.html + --ignore-url .*/plutus-core/Control-Monad-Trans-State-Lazy.html + --ignore-url .*/plutus-core/Control-Monad-Trans-State-Strict.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Writer-CPS.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Writer-Lazy.html + --ignore-url .*/plutus-core/Control-Monad-Trans-Writer-Strict.html + --ignore-url .*/plutus-core/Control-Search.html + --ignore-url .*/plutus-core/CostModelGeneration.html + --ignore-url .*/plutus-core/Crypto-ECC-Ed25519Donna.html + --ignore-url .*/plutus-core/Crypto-Error-Types.html + --ignore-url .*/plutus-core/Crypto-Hash-Types.html + --ignore-url .*/plutus-core/Data-Aeson-Key.html + --ignore-url .*/plutus-core/Data-Aeson-KeyMap.html + --ignore-url .*/plutus-core/Data-Aeson-Types-FromJSON.html + --ignore-url .*/plutus-core/Data-Aeson-Types-Internal.html + --ignore-url .*/plutus-core/Data-Aeson-Types-ToJSON.html + --ignore-url .*/plutus-core/Data-Attoparsec-Internal-Types.html + --ignore-url .*/plutus-core/Data-Bifunctor-Biff.html + --ignore-url .*/plutus-core/Data-Bifunctor-Clown.html + --ignore-url .*/plutus-core/Data-Bifunctor-Fix.html + --ignore-url .*/plutus-core/Data-Bifunctor-Flip.html + --ignore-url .*/plutus-core/Data-Bifunctor-Join.html + --ignore-url .*/plutus-core/Data-Bifunctor-Joker.html + --ignore-url .*/plutus-core/Data-Bifunctor-Product.html + --ignore-url .*/plutus-core/Data-Bifunctor-Sum.html + --ignore-url .*/plutus-core/Data-Bifunctor-Tannen.html + --ignore-url .*/plutus-core/Data-Bifunctor-Wrapped.html + --ignore-url .*/plutus-core/Data-Bimap.html + --ignore-url .*/plutus-core/Data-ByteString-Convert.html + --ignore-url .*/plutus-core/Data-ByteString-Internal-Type.html + --ignore-url .*/plutus-core/Data-ByteString-Lazy-Internal.html + --ignore-url .*/plutus-core/Data-ByteString-Short-Internal.html + --ignore-url .*/plutus-core/Data-Csv-Conversion.html + --ignore-url .*/plutus-core/Data-DList-DNonEmpty-Internal.html + --ignore-url .*/plutus-core/Data-DList-Internal.html + --ignore-url .*/plutus-core/Data-Default-Class.html + --ignore-url .*/plutus-core/Data-Dependent-Sum.html + --ignore-url .*/plutus-core/Data-Fix.html + --ignore-url .*/plutus-core/Data-Functor-Base.html + --ignore-url .*/plutus-core/Data-Functor-Constant.html + --ignore-url .*/plutus-core/Data-Functor-Foldable.html + --ignore-url .*/plutus-core/Data-Functor-Reverse.html + --ignore-url .*/plutus-core/Data-Functor-These.html + --ignore-url .*/plutus-core/Data-Functor-Yoneda.html + --ignore-url .*/plutus-core/Data-GADT-DeepSeq.html + --ignore-url .*/plutus-core/Data-GADT-Internal.html + --ignore-url .*/plutus-core/Data-HashMap-Internal-Array.html + --ignore-url .*/plutus-core/Data-HashMap-Internal.html + --ignore-url .*/plutus-core/Data-HashMap-Monoidal.html + --ignore-url .*/plutus-core/Data-HashSet-Internal.html + --ignore-url .*/plutus-core/Data-Hashable-Class.html + --ignore-url .*/plutus-core/Data-IntMap-Internal.html + --ignore-url .*/plutus-core/Data-IntSet-Internal.html + --ignore-url .*/plutus-core/Data-Map-Internal.html + --ignore-url .*/plutus-core/Data-MonoTraversable.html + --ignore-url .*/plutus-core/Data-MultiSet.html + --ignore-url .*/plutus-core/Data-Primitive-Array.html + --ignore-url .*/plutus-core/Data-Primitive-PrimArray.html + --ignore-url .*/plutus-core/Data-Primitive-SmallArray.html + --ignore-url .*/plutus-core/Data-Primitive-Types.html + --ignore-url .*/plutus-core/Data-Profunctor-Choice.html + --ignore-url .*/plutus-core/Data-Profunctor-Closed.html + --ignore-url .*/plutus-core/Data-Profunctor-Composition.html + --ignore-url .*/plutus-core/Data-Profunctor-Mapping.html + --ignore-url .*/plutus-core/Data-Profunctor-Strong.html + --ignore-url .*/plutus-core/Data-Profunctor-Types.html + --ignore-url .*/plutus-core/Data-Profunctor-Unsafe.html + --ignore-url .*/plutus-core/Data-RAList-Tree-Internal.html + --ignore-url .*/plutus-core/Data-Reflection.html + --ignore-url .*/plutus-core/Data-Scientific.html + --ignore-url .*/plutus-core/Data-Semigroup-Traversable-Class.html + --ignore-url .*/plutus-core/Data-Sequence-Internal.html + --ignore-url .*/plutus-core/Data-Sequences.html + --ignore-url .*/plutus-core/Data-Set-Internal.html + --ignore-url .*/plutus-core/Data-Some-GADT.html + --ignore-url .*/plutus-core/Data-Some-Newtype.html + --ignore-url .*/plutus-core/Data-Stream.html + --ignore-url .*/plutus-core/Data-Strict-Either.html + --ignore-url .*/plutus-core/Data-Strict-Maybe.html + --ignore-url .*/plutus-core/Data-Strict-These.html + --ignore-url .*/plutus-core/Data-Strict-Tuple.html + --ignore-url .*/plutus-core/Data-Tagged.html + --ignore-url .*/plutus-core/Data-Text-Encoding-Error.html + --ignore-url .*/plutus-core/Data-Text-Short-Internal.html + --ignore-url .*/plutus-core/Data-These.html + --ignore-url .*/plutus-core/Data-Time-Calendar-Days.html + --ignore-url .*/plutus-core/Data-Time-Clock-Internal-DiffTime.html + --ignore-url .*/plutus-core/Data-Time-Clock-Internal-NominalDiffTime.html + --ignore-url .*/plutus-core/Data-Time-Clock-Internal-UTCTime.html + --ignore-url .*/plutus-core/Data-Time-Clock-Internal-UniversalTime.html + --ignore-url .*/plutus-core/Data-Time-LocalTime-Internal-LocalTime.html + --ignore-url .*/plutus-core/Data-Time-LocalTime-Internal-ZonedTime.html + --ignore-url .*/plutus-core/Data-Tree.html + --ignore-url .*/plutus-core/Data-Tuple-Only.html + --ignore-url .*/plutus-core/Data-UUID-Types-Internal-Builder.html + --ignore-url .*/plutus-core/Data-UUID-Types-Internal.html + --ignore-url .*/plutus-core/Data-Vector-Primitive.html + --ignore-url .*/plutus-core/Data-Vector-Storable.html + --ignore-url .*/plutus-core/Data-Vector-Unboxed-Base.html + --ignore-url .*/plutus-core/Data-Vector.html + --ignore-url .*/plutus-core/Data.html + --ignore-url .*/plutus-core/Flat-Decoder-Types.html + --ignore-url .*/plutus-core/Flat-Filler.html + --ignore-url .*/plutus-core/GHC-Exts-Heap-ClosureTypes.html + --ignore-url .*/plutus-core/GHC-Exts-Heap-Closures.html + --ignore-url .*/plutus-core/GHC-Exts-Heap-InfoTable-Types.html + --ignore-url .*/plutus-core/GHC-Exts-Heap-ProfInfo-Types.html + --ignore-url .*/plutus-core/Hedgehog-Internal-Gen.html + --ignore-url .*/plutus-core/Hedgehog-Internal-Property.html + --ignore-url .*/plutus-core/Hedgehog-Internal-Tree.html + --ignore-url .*/plutus-core/Inline-CallSiteInline.html + --ignore-url .*/plutus-core/Language-Haskell-TH-Datatype.html + --ignore-url .*/plutus-core/Lens-Micro-Internal.html + --ignore-url .*/plutus-core/ListT.html + --ignore-url .*/plutus-core/N + --ignore-url .*/plutus-core/Network-URI.html + --ignore-url .*/plutus-core/NoThunks-Class.html + --ignore-url .*/plutus-core/Numeric-Half-Internal.html + --ignore-url .*/plutus-core/PLC.html + --ignore-url .*/plutus-core/PlutusLedgerApi-Common-SerialisedScript.html + --ignore-url .*/plutus-core/Prettyprinter-Internal.html + --ignore-url .*/plutus-core/Prismatically.html + --ignore-url .*/plutus-core/System-Console-Terminal-Common.html + --ignore-url .*/plutus-core/System-OsString-Internal-Types-Hidden.html + --ignore-url .*/plutus-core/System-Random-Internal.html + --ignore-url .*/plutus-core/System-Random-Stateful.html + --ignore-url .*/plutus-core/Test-QuickCheck-Arbitrary.html + --ignore-url .*/plutus-core/Test-QuickCheck-Function.html + --ignore-url .*/plutus-core/Test-QuickCheck-Gen.html + --ignore-url .*/plutus-core/Test-QuickCheck-GenT-Private.html + --ignore-url .*/plutus-core/Test-QuickCheck-GenT.html + --ignore-url .*/plutus-core/Test-QuickCheck-Modifiers.html + --ignore-url .*/plutus-core/Test-QuickCheck-Property.html + --ignore-url .*/plutus-core/Text-Megaparsec-Error.html + --ignore-url .*/plutus-core/Text-Megaparsec-Internal.html + --ignore-url .*/plutus-core/Text-Megaparsec-Pos.html + --ignore-url .*/plutus-core/Text-Megaparsec-State.html + --ignore-url .*/plutus-core/Text-PrettyPrint-Annotated-WL.html + --ignore-url .*/plutus-core/Utils.html + --ignore-url .*/plutus-core/WithIndex.html + --ignore-url .*/plutus-core/Witherable.html + --ignore-url .*/plutus-core/a_non_- + --ignore-url .*/plutus-core/folder + --ignore-url .*/plutus-core/input + --ignore-url .*/plutus-core/just_case_body + --ignore-url .*/plutus-core/name + --ignore-url .*/plutus-core/nothing_case_body + --ignore-url .*/plutus-ghc-stub/= + --ignore-url .*/plutus-ledger-api/Alonzo.html + --ignore-url .*/plutus-ledger-api/Control-Lens-Wrapped.html + --ignore-url .*/plutus-ledger-api/Control-Monad-Error-Class.html + --ignore-url .*/plutus-ledger-api/Control-Monad-Free.html + --ignore-url .*/plutus-ledger-api/Control-Monad-Trans-Free.html + --ignore-url .*/plutus-ledger-api/Control-Monad-Trans-Resource-Internal.html + --ignore-url .*/plutus-ledger-api/Crypto.html + --ignore-url .*/plutus-ledger-api/Data-Aeson-Types-FromJSON.html + --ignore-url .*/plutus-ledger-api/Data-Aeson-Types-ToJSON.html + --ignore-url .*/plutus-ledger-api/Data-Functor-Rep.html + --ignore-url .*/plutus-ledger-api/Data-Profunctor-Choice.html + --ignore-url .*/plutus-ledger-api/Data-Profunctor-Rep.html + --ignore-url .*/plutus-ledger-api/Data-Profunctor-Unsafe.html + --ignore-url .*/plutus-ledger-api/Data-Semigroup-Traversable-Class.html + --ignore-url .*/plutus-ledger-api/Data-Tagged.html + --ignore-url .*/plutus-ledger-api/Data-Time-Clock-POSIX.html + --ignore-url .*/plutus-ledger-api/GHC.html + --ignore-url .*/plutus-ledger-api/Hedgehog-Internal-Gen.html + --ignore-url .*/plutus-ledger-api/Hedgehog-Internal-Property.html + --ignore-url .*/plutus-ledger-api/Hedgehog-Internal-Tree.html + --ignore-url .*/plutus-ledger-api/ListT.html + --ignore-url .*/plutus-ledger-api/Prettyprinter-Internal.html + --ignore-url .*/plutus-tx-plugin/level + --ignore-url .*/plutus-tx/- + --ignore-url .*/plutus-tx/Algebra-Graph-Class.html + --ignore-url .*/plutus-tx/Basement-Bits.html + --ignore-url .*/plutus-tx/Basement-Monad.html + --ignore-url .*/plutus-tx/Basement-Numerical-Subtractive.html + --ignore-url .*/plutus-tx/Codec-Serialise-Class.html + --ignore-url .*/plutus-tx/Comment.html + --ignore-url .*/plutus-tx/Control-Lens-At.html + --ignore-url .*/plutus-tx/Control-Lens-Each.html + --ignore-url .*/plutus-tx/Control-Lens-Empty.html + --ignore-url .*/plutus-tx/Control-Monad-Error-Class.html + --ignore-url .*/plutus-tx/Control-Monad-Trans-Control.html + --ignore-url .*/plutus-tx/Data-Aeson-Types-FromJSON.html + --ignore-url .*/plutus-tx/Data-Aeson-Types-ToJSON.html + --ignore-url .*/plutus-tx/Data-Default-Class.html + --ignore-url .*/plutus-tx/Data-Functor-Foldable.html + --ignore-url .*/plutus-tx/Data-Hashable-Class.html + --ignore-url .*/plutus-tx/Data-Map-Lazy.html + --ignore-url .*/plutus-tx/Data-MonoTraversable.html + --ignore-url .*/plutus-tx/Data-Reflection.html + --ignore-url .*/plutus-tx/Data-Semigroup-Traversable-Class.html + --ignore-url .*/plutus-tx/Data-Vector-Unboxed-Base.html + --ignore-url .*/plutus-tx/Data.html + --ignore-url .*/plutus-tx/Description.html + --ignore-url .*/plutus-tx/GHC.html + --ignore-url .*/plutus-tx/Lens-Micro-Internal.html + --ignore-url .*/plutus-tx/P.html + --ignore-url .*/plutus-tx/PlutusTx-AssocMap-Map.html + --ignore-url .*/plutus-tx/Prettyprinter-Internal.html + --ignore-url .*/plutus-tx/Safe.html + --ignore-url .*/plutus-tx/System-Random-Internal.html + --ignore-url .*/plutus-tx/Text-PrettyPrint-Annotated-WL.html + --ignore-url .*/plutus-tx/Title.html + --ignore-url .*/plutus-tx/Unrolling.html + --ignore-url .*/plutus-tx/WithIndex.html + --ignore-url .*/prettyprinter-configurable/Prettyprinter.html + --ignore-url .*/plutus-core/src + --ignore-url .*/plutus-tx/src + --ignore-url .*/prettyprinter-configurable/src + ) URL="https://plutus.cardano.intersectmbo.org/haddock/${{ inputs.destination || github.ref_name }}" - linkchecker --no-status --no-warnings --check-extern --output failures "${URL}" + linkchecker --no-warnings --check-extern --output failures "${URL}" "${IGNORE_URLS}" if [ $? -ne 0 ]; then echo "${URL}" has broken links, see output above" exit 1 - fi \ No newline at end of file + fi + + + \ No newline at end of file diff --git a/.github/workflows/metatheory-site.yml b/.github/workflows/metatheory-site.yml index 7b848cac4fd..4b0cc67ae79 100644 --- a/.github/workflows/metatheory-site.yml +++ b/.github/workflows/metatheory-site.yml @@ -36,7 +36,7 @@ jobs: - name: Check Broken Links run: | URL="https://plutus.cardano.intersectmbo.org/metatheory" - linkchecker --no-status --no-warnings --check-extern --output failures "${URL}" + linkchecker --no-warnings --check-extern --output failures "${URL}" if [ $? -ne 0 ]; then echo "${URL}" has broken links, see output above" exit 1 diff --git a/scripts/check-broken-links.sh b/scripts/check-broken-links.sh index 3dd731f0866..72e707b71c2 100755 --- a/scripts/check-broken-links.sh +++ b/scripts/check-broken-links.sh @@ -16,7 +16,7 @@ grep_links() { } check_links() { - linkchecker --no-status --no-warnings --recursion-level 0 --output failures --check-extern "${IGNORE_URLS[@]}" --stdin + linkchecker --no-warnings --recursion-level 0 --output failures --check-extern "${IGNORE_URLS[@]}" --stdin } for file in $(find "${TARGETS[@]}"); do diff --git a/scripts/combined-haddock.sh b/scripts/combined-haddock.sh index a06db53c75e..f73d9114663 100755 --- a/scripts/combined-haddock.sh +++ b/scripts/combined-haddock.sh @@ -222,8 +222,7 @@ fi echo "Running linkchecker" -time linkchecker --no-status "${OUTPUT_DIR}/index.html" \ - --check-extern \ +time linkchecker "${OUTPUT_DIR}/index.html" \ --no-warnings \ --output failures \ --file-output text From fdea162828b44023cf2ce07b9c2ea46867aca789 Mon Sep 17 00:00:00 2001 From: zeme Date: Mon, 8 Jul 2024 12:35:23 +0200 Subject: [PATCH 5/8] wip --- .github/workflows/docusaurus-site.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docusaurus-site.yml b/.github/workflows/docusaurus-site.yml index 2d02c0e80f8..117e5a57219 100644 --- a/.github/workflows/docusaurus-site.yml +++ b/.github/workflows/docusaurus-site.yml @@ -35,12 +35,12 @@ jobs: - name: Check Broken Links run: | IGNORE_URLS=( - --ignore-url https://plutus.cardano.intersectmbo.org/docs/haddock/.* + --ignore-url "https://plutus.cardano.intersectmbo.org/docs/haddock/.*" ) URL="https://plutus.cardano.intersectmbo.org/docs" - linkchecker --no-warnings --check-extern --output failures "${URL}" "${IGNORE_URL}" + linkchecker --no-warnings --check-extern --output failures "${URL}" "${IGNORE_URLS[@]}" if [ $? -ne 0 ]; then - echo "${URL}" has broken links, see output above" + echo "${URL} has broken links, see output above" exit 1 fi \ No newline at end of file From b09d8d6d1eb6d76430c2cb7c22257b302dbf6751 Mon Sep 17 00:00:00 2001 From: zeme Date: Mon, 8 Jul 2024 12:39:56 +0200 Subject: [PATCH 6/8] wip --- plutus-metatheory/README.md | 230 ------------------------------------ 1 file changed, 230 deletions(-) diff --git a/plutus-metatheory/README.md b/plutus-metatheory/README.md index 5bc3d1bff22..8bc5198331e 100644 --- a/plutus-metatheory/README.md +++ b/plutus-metatheory/README.md @@ -101,233 +101,3 @@ $ jekyll build -s html -d html/_site ## Detailed Description See the [table of contents](https://plutus.cardano.intersectmbo.org/metatheory/) for an explanation of the structure of the formalisation and links to the code. - -**The below information is deprecated and is in the process of being -replaced by the table of contents document.** - -## Structure of the intrinsically typed formalisation - -The intrinsic formalisation is split into three sections. Firstly, - -1. Types. - -Then, two different implementations of the term language: - -2. Terms indexed by syntactic types (declarative); -3. Terms indexed by normal types (algorithmic). - -## Types - -Types are defined in the -[Type](https://plutus.cardano.intersectmbo.org/metatheory/Type.html) -module. They are intrinsically kinded so it is impossible to apply a -type operator to arguments of the wrong kind. - -The type module is further subdivided into submodules: - -1. [Type.RenamingSubstitution](https://plutus.cardano.intersectmbo.org/metatheory/Type.RenamingSubstitution.html) -contains the operations of renaming and substitution for types and -their proofs of correctness. These are necessary to, for example, -define the beta rule for types in the equational theory and reduction -relation (described below). - -2. [Type.Equality](https://plutus.cardano.intersectmbo.org/metatheory/Type.Equality.html) contains the beta-equational -theory of types. This is essentially a specification for the -computational behaviour of types. - -3. [Type.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Type.Reduction.html) contains the small step -reduction relation, the progress/preservation results for types, and -an evaluator for types. This result is not used later in the -development but is in the spec. - -4. [Type.BetaNormal](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNormal.html) contains beta normal forms -for types as a separate syntax. Beta normal forms contain no -beta-redexes and guaranteed not to compute any further. - -5. [Type.BetaNBE](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.html) contains a beta normaliser for -types, it is defined in the style of "normalization-by-evaluation" -(NBE) and is guaranteed to terminate. Further submodules define the -correctness proofs for the normalizer and associated operations. - - 1. [Type.BetaNBE.Soundness](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.Soundness.html) contains a - proof that normalizer preserves the meaning of the types. Formally it - states that if we normalize a type then the resultant normal form is - equal (in the equational theory) to the type we started with. - - 2. [Type.BetaNBE.Completeness](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.Completeness.html) - contains a proof that the if we were to normalize two types that are - equal in the equation theory then we will end up with identical normal - forms. - - 3. [Type.BetaNBE.Stability](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.Stability.html) contains a - proof that normalization will preserve syntactic structure of terms - already in normal form. - - 4. [Type.BetaNBE.RenamingSubsitution](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.RenamingSubstitution.html) - contains a version of substitution that works on normal forms and - ensures that the result is in normal form. This works by embedding - normal forms back into syntax, performing a syntactic substitution and - then renormalizing. The file also contains a correctness proof for - this version of substitution. - -Note: Crucially, this development of NBE (and anything else in the -formalisation for that matter) does not rely on any postulates -(axioms). Despite the fact that we need to reason about functions in -several places we do not require appealing to function extensionality -which currently requires a postulate in Agda. In this formalisation -the (object) type level programs and their proofs appear in (object) -terms. Appealing to a postulate in type level proofs would stop term -level programs computing. - -## Builtins - -There are builtin types of integers and bytestrings. - -1. [Builtin.Constant.Type](https://plutus.cardano.intersectmbo.org/metatheory/Builtin.Constant.Type.html) -contains the enumeration of the type constants. -2. [Builtin.Constant.Term](https://plutus.cardano.intersectmbo.org/metatheory/Builtin.Constant.Term.html) -contains the enumeration of the term constants at the bottom. -3. [Builtin.Signature](https://plutus.cardano.intersectmbo.org/metatheory/Builtin.Signature.html) -contains the list of builtin operations and their type signatures. In -the specification this information is contained in the large builtin -table. - -The rest of the Builtin machinery: telescopes, and the semantics of -builtins are contained in -[Declarative.Term.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.Reduction.html). - -## Terms indexed by syntactic types - -This is the standard presentation of the typing rules that one may -find in a text book. We can define the terms easily in this style but -using them in further programs/proofs is complicated by the presence -of a separate syntactic constructor for type conversion (type -cast/coercion). The typing rules are not syntax directed which means -it is not possible to directly write a typechecker for these rules as -their is always a choice of rules to apply when building a -derivation. Hence we refer to this version as declarative rather than -algorithmic. In this formalisation where conversion is a constructor -of the syntax not just a typing rule this also affects computation as -we don't know how to process conversions when evaluating. In this -version progress, and evaluation do not handle the conversion -constructor. They fail if they encounter it. Nevertheless this is -sufficient to handle examples which do not require computing the types -before applying beta-reductions. Such as Church/Scott Numerals. - -1. The [Declarative.Term](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.html) -module contains the definition of terms. This module has two further submodules: - - 1. [Declarative.Term.RenamingSubstitution](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.RenamingSubstitution.html) - contains the definitions of substitution for terms that is necessary to - specify the beta-rules in the reduction relation. This definition and - those it depends on, in turn, depend on the definitions and correctness - proofs of the corresponding type level operations. - - 2. [Declarative.Term.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.Reduction.html) - This file contains the reduction relation for terms (also known - as the small step operational semantics) and the progress proof. - Preservation is inherent. Note: this version of - progress doesn't handle type conversions in terms. - -2. [Declarative.Evaluation](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Evaluation.html) -contains the evaluator the terms. It takes a *gas* argument which is -the number of steps of reduction that are allowed. It returns both a -result and trace of reduction steps or *out of gas*. Note: this -version of evaluation doesn't handle type conversions in terms. - -3. [Declarative.Examples](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Examples.html) -contains some examples of Church and Scott Numerals. Currently it is -very memory intensive to type check this file and/or run examples. - -4. [Erasure](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Erasure.html) - -## Terms indexed by normal types - -This version is able to handle type conversion by using the normalizer -described above to ensure that types are always in normal form. This -means that no conversion constructor is necessary as any two types -which one could convert between are already in identical normal -form. Here the typing rules are syntax directed and we don't have to -deal with conversions in the syntax. This allows us to define -progress, preservation, and evaluation for the full language of System -F omega with iso-recursive types and sized integers and bytestrings. - -1. The [Algorithmic.Term](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Term.html) -module contains the definition of terms. This module has two further submodules: - - 1. [Algorithmic.Term.RenamingSubstitution](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Term.RenamingSubstitution.html) - contains the definitions of substitution for terms that is - necessary to specify the beta-rules in the reduction - relation. This definition and those it depends on, in turn, - depend on the definitions and correctness proofs of the - corresponding type level operations. In this version this - includes depeneding on the correctness proof of the beta - normalizer for types. - - 2. [Algorithmic.Term.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Term.Reduction.html) - This file contains the reduction relation for terms (also known - as the small step operational semantics) and the progress proof. - Preservation is, again, inherent. - -2. [Algorithmic.Evaluation](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Evaluation.html) -contains the evaluator the terms. It takes a *gas* argument which is -the number of steps of reduction that are allowed. It returns both a -result and trace of reduction steps or *out of gas*. - -3. [Algorithmic.Examples](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Examples.html) -contains some examples of Church and Scott Numerals. Currently it is -very memory intensive to type check this file and/or run examples. - -We also need to show that the algorithmic version of the type system is sound and complete. - -4. [Algorithmic.Soundness](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Soundness.html) - -Programmatically this corresponds to taking a term with normal type -and converting it back to a term with a syntactic type. This -introduces conversions into the term anywhere there a substitution -occurs in a type. - -4. [Algorithmic.Completeness](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Completeness.html) - -5. [Erasure](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Erasure.html) contains erasure to untyped lambda calculus. - -Programmatically this correponds to taking a term with a syntactic -type that may contain conversions and normalising its type by -collapsing all the conversions. - -# Extrinsically typed version - -1. [Syntax](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.html) -contains the intrinsically scoped but extrinsically typed terms, and -intrinsically scoped but extrinscically kinded types. - -2. [Renaming and -Substitution](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.RenamingSubstitution.html) -contains the operations of renaming and substitution for extrinsically -typed terms, and extrinsically kinded types. - -3. [Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Reduction.html) contains the reduction rules, progress and evaluation. - -4. [Extrication](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Extrication.html) -contains the operations to convert from intrinsically typed to -extrinscally typed syntax. - -5. [Erasure](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Erasure.html) -contains operations to erase the types yielding untyped terms. - - 1. [Renaming and - Substitution](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Erasure.RenamingSubstitution.html) - contains operations to erase the types in extrinsic renamings and - substitutions yielding untyped renamings and substitutions. - -# Untyped version - -1. [Syntax](https://plutus.cardano.intersectmbo.org/metatheory/Untyped.html) -contains intrinsically scoped but untyped lambda calculus extended -with builtins. - -2. [Renaming and -Substitution](https://plutus.cardano.intersectmbo.org/metatheory/Untyped.RenamingSubstitution.html) -contains operations for untyped renaming and substitution. - -3. [Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Untyped.Reduction.html) contains the untyped reduction rules. From d3173dac2b6fb0d1048d7976ca67362f289e4541 Mon Sep 17 00:00:00 2001 From: Ramsay Taylor Date: Mon, 8 Jul 2024 11:42:41 +0100 Subject: [PATCH 7/8] Minor rewording. --- plutus-metatheory/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plutus-metatheory/README.md b/plutus-metatheory/README.md index 8bc5198331e..50bef7ca638 100644 --- a/plutus-metatheory/README.md +++ b/plutus-metatheory/README.md @@ -100,4 +100,4 @@ $ jekyll build -s html -d html/_site ## Detailed Description -See the [table of contents](https://plutus.cardano.intersectmbo.org/metatheory/) for an explanation of the structure of the formalisation and links to the code. +See the site generated from the [Literate Agda](https://plutus.cardano.intersectmbo.org/metatheory/) for an explanation of the structure of the formalisation and links to the code. From 963f97ac9bb7a4089bcac796e304fd00903c4d00 Mon Sep 17 00:00:00 2001 From: zeme Date: Mon, 8 Jul 2024 12:49:34 +0200 Subject: [PATCH 8/8] wip --- .github/workflows/docusaurus-site.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docusaurus-site.yml b/.github/workflows/docusaurus-site.yml index 117e5a57219..a71639621f7 100644 --- a/.github/workflows/docusaurus-site.yml +++ b/.github/workflows/docusaurus-site.yml @@ -35,7 +35,7 @@ jobs: - name: Check Broken Links run: | IGNORE_URLS=( - --ignore-url "https://plutus.cardano.intersectmbo.org/docs/haddock/.*" + --ignore-url "https://plutus.cardano.intersectmbo.org/haddock/.*" ) URL="https://plutus.cardano.intersectmbo.org/docs" linkchecker --no-warnings --check-extern --output failures "${URL}" "${IGNORE_URLS[@]}"