From 92f390c3a3ae570f17d90645c8fa52f026f8cfea Mon Sep 17 00:00:00 2001 From: zeme-wana <15709674+zeme-wana@users.noreply.github.com> Date: Mon, 8 Jul 2024 15:43:51 +0200 Subject: [PATCH] Detect broken links for haddock,metatheory,docusaurus + local repo files (#6294) --- .github/ISSUE_TEMPLATE/bug_report.yml | 2 +- .github/ISSUE_TEMPLATE/feature_request.yml | 2 +- .github/workflows/broken-links.yml | 27 +- .github/workflows/docusaurus-site.yml | 16 +- .github/workflows/haddock-site.yml | 295 +++++++++++++++++- .github/workflows/longitudinal-benchmark.yml | 4 +- .github/workflows/metatheory-site.yml | 52 +-- .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 | 6 +- 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 | 232 +------------- plutus-metatheory/src/Builtin.lagda.md | 6 +- .../src/Type/RenamingSubstitution.lagda.md | 4 +- scripts/check-broken-links.sh | 33 +- scripts/combined-haddock.sh | 1 - 23 files changed, 378 insertions(+), 356 deletions(-) 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/workflows/broken-links.yml b/.github/workflows/broken-links.yml index 5fcf01ec61e..536a8249a2d 100644 --- a/.github/workflows/broken-links.yml +++ b/.github/workflows/broken-links.yml @@ -1,24 +1,12 @@ -# This job checks for broken links in the various files. - +# 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: check: @@ -30,4 +18,7 @@ jobs: - name: Run Linkchecker 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 + + + diff --git a/.github/workflows/docusaurus-site.yml b/.github/workflows/docusaurus-site.yml index eaca8024536..a71639621f7 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,16 @@ jobs: folder: doc/docusaurus/build target-folder: docs single-commit: true - + + - name: Check Broken Links + run: | + IGNORE_URLS=( + --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[@]}" + 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..99dee8f8106 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,287 @@ 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: | + 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-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 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..4b0cc67ae79 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://intersectmbo.github.io/plutus/metatheory/$version -# And optionally to: -# https://intersectmbo.github.io/plutus/metatheory/latest -# On push to master, this workflows publishes to: -# https://intersectmbo.github.io/plutus/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://intersectmbo.github.io/plutus/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. - 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,14 +30,14 @@ 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" + linkchecker --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..20fd04c9174 100644 --- a/doc/docusaurus/docusaurus.config.ts +++ b/doc/docusaurus/docusaurus.config.ts @@ -8,14 +8,10 @@ const config: Config = { favicon: "img/favicon.ico", // Set the production url of your site here - url: "https://intersectmbo.github.io", + 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..50bef7ca638 100644 --- a/plutus-metatheory/README.md +++ b/plutus-metatheory/README.md @@ -100,234 +100,4 @@ $ 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. - -**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://input-output-hk.github.io/plutus-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) -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 -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 -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 -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 -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 - 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) - 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 - 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) - 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://input-output-hk.github.io/plutus-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) -contains the enumeration of the term constants at the bottom. -3. [Builtin.Signature](https://input-output-hk.github.io/plutus-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). - -## 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://input-output-hk.github.io/plutus-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) - 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) - 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) -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) -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) - -## 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://input-output-hk.github.io/plutus-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) - 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://input-output-hk.github.io/plutus-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) -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) -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) - -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) - -5. [Erasure](https://input-output-hk.github.io/plutus-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://input-output-hk.github.io/plutus-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) -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. - -4. [Extrication](https://input-output-hk.github.io/plutus-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) -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) - 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) -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) -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. +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. 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..72e707b71c2 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-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..f73d9114663 100755 --- a/scripts/combined-haddock.sh +++ b/scripts/combined-haddock.sh @@ -223,7 +223,6 @@ fi echo "Running linkchecker" time linkchecker "${OUTPUT_DIR}/index.html" \ - --check-extern \ --no-warnings \ --output failures \ --file-output text