plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.36k stars 307 forks source link

Type mismatch when `make build` #965

Closed OlingCat closed 7 months ago

OlingCat commented 7 months ago

I tried to make build PLFA and encountered the following error:

$ make build
Building PLFA...
cabal  v2-update
Downloading the latest package list from mirrors.ustc.edu.cn
Package list of mirrors.ustc.edu.cn is up to date.
The index-state is set to 2024-02-20T21:39:04Z.
cabal  v2-run builder -- build -j --lint --profile=_cache/reports/build.html --timing
Build profile: -w ghc-9.4.8 -O1
In order, the following will be built (use -v for more details):
 - plfa-22.8 (exe:builder) (first run)
Preprocessing executable 'builder' for plfa-22.8..
Building executable 'builder' for plfa-22.8..
[1 of 1] Compiling Main             ( tools/Buildfile.hs, /mnt/d/Source/plfa/dist-newstyle/build/x86_64-linux/ghc-9.4.8/plfa-22.8/x/builder/build/builder/builder-tmp/Main.o )

tools/Buildfile.hs:273:28: error:
    • Couldn't match type ‘base64-1.0:Data.Base64.Types.Internal.Base64
                             'base64-1.0:Data.Base64.Types.Internal.StdPadded LazyText.Text’
                     with ‘LazyText.Text’
        arising from a functional dependency between constraints:
          ‘?getDigest::FilePath -> Action (Maybe LazyText.Text)’
            arising from a use of ‘getStylesheetField’ at tools/Buildfile.hs:273:28-45
          ‘?getDigest::FilePath
                       -> Action
                            (Maybe
                               (base64-1.0:Data.Base64.Types.Internal.Base64
                                  'base64-1.0:Data.Base64.Types.Internal.StdPadded LazyText.Text))’
            arising from the implicit-parameter binding for ?getDigest at tools/Buildfile.hs:229:7-15
    • In a stmt of a 'do' block: stylesheetField <- getStylesheetField
      In the expression:
        do src <- Route.source out
           tocField <- getTableOfContentsField ()
           (fileMetadata, indexMarkdownTemplate) <- getFileWithMetadata src
           stylesheetField <- getStylesheetField
           ....
      In the second argument of ‘(%>)’, namely
        ‘\ out
           -> do src <- Route.source out
                 tocField <- getTableOfContentsField ()
                 ....’
    |
273 |         stylesheetField <- getStylesheetField
    |                            ^^^^^^^^^^^^^^^^^^
make: *** [Makefile:33: build] Error 1

Here is my building environment:

$ cabal --version
cabal-install version 3.10.2.1
compiled using version 3.10.2.1 of the Cabal library

$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 9.4.8

$ agda --version
Agda version 2.6.3

This issue can be reproduced on Windows 11 and Archlinux/Ubuntu in WSL.

wenkokke commented 7 months ago

This can probably be fixed with an upper bound on the base64 package.

wenkokke commented 7 months ago

Fixed.