Regarding the Haskell errors, do you have warnings-as-errors on? It seems like all of the errors are actually just promoted warnings, so possibly you can just disable those warnings.
On Mon, Mar 18, 2024 at 4:59 PM Antony Bartlett <[email protected]> wrote: > I've been trying to add hmm to metamath-docker, because it's one of the > verifiers that metamath-test is set up to run against. > > The more I think about it, the more any attempt to maintain metamath-test > without containerization seems insane. You need to have C, C++, Rust, > Java, Python, and Haskell installed, then use them to build metamath.exe, > checkmm, metamath-knife, mmj2, mmverifypy, and hmm respectively in order to > be able to run ./run-testsuite-all-drivers > > Respect to David Wheeler for getting it all running in the first place! > > The README (http://home.solcon.nl/mklooster/repos/hmm/README) says hmm > was developed with GHC 6.4, and this is almost certainly the problem > because neither the apt or apk package manager repositories seem to go back > any further than the current major version of Haskell, GHC 9.x > > Any suggestions? I'm afraid it's not my programming language, so I'm not > going to be able to upgrade it myself. > > For the sake of completeness my attempted changes look like this > https://github.com/Antony74/metamath-docker/compare/main...add-haskell-verifier > > # hmm: dependencies for building Haskell programs > RUN apk add --no-cache ghc > # hmm: get and build > WORKDIR /build > RUN curl https://us.metamath.org/downloads/hmm.zip -o hmm.zip > RUN unzip hmm.zip -d . > WORKDIR /build/hmm > # RUN make > And the errors I get when I run make: > > /build/hmm # make > ghc -Wall -Werror -O -o hmmTest --make HmmTest > [1 of 3] Compiling HmmImpl ( HmmImpl.hs, HmmImpl.o ) > > HmmImpl.hs:37:1: error: [-Wtabs, -Werror=tabs] > Tab character found here, and in 756 further locations. > Suggested fix: Please use spaces instead. > | > 37 | deriving (Eq, Show) > | ^^^^^^^^ > > HmmImpl.hs:94:40: error: [-Wincomplete-uni-patterns, > -Werror=incomplete-uni-patterns] > Pattern match(es) are non-exhaustive > In a pattern binding: > Patterns of type ‘Expression’ not matched: > [] > ((Var _):_) > [(Con _)] > ((Con _):(Con _):_) > ... > | > 94 | DollarF -> let [Con _c, Var v] = syms in > | ^^^^^^^^^^^^^^^^^^^^^^ > > HmmImpl.hs:219:17: error: [-Wunused-do-bind, -Werror=unused-do-bind] > A do-notation statement discarded a result of type ‘[()]’ > Suggested fix: > Suppress this warning by saying > ‘_ <- many1 ((space >> return ()) <|> mmpComment)’ > | > 219 | many1 ((space >> return ()) <|> mmpComment) > | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > > HmmImpl.hs:224:17: error: [-Wunused-do-bind, -Werror=unused-do-bind] > A do-notation statement discarded a result of type ‘String’ > Suggested fix: > Suppress this warning by saying ‘_ <- try (string "$(")’ > | > 224 | try (string "$(") > | ^^^^^^^^^^^^^^^^^ > > HmmImpl.hs:225:17: error: [-Wunused-do-bind, -Werror=unused-do-bind] > A do-notation statement discarded a result of type ‘[Char]’ > Suggested fix: > Suppress this warning by saying > ‘_ <- manyTill anyChar (try (space >> string "$)"))’ > | > 225 | manyTill anyChar (try (space >> string "$)")) > | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > > HmmImpl.hs:279:17: error: [-Wunused-do-bind, -Werror=unused-do-bind] > A do-notation statement discarded a result of type ‘String’ > Suggested fix: Suppress this warning by saying ‘_ <- string "$."’ > | > 279 | string "$." > | ^^^^^^^^^^^ > > HmmImpl.hs:319:17: error: [-Wunused-do-bind, -Werror=unused-do-bind] > A do-notation statement discarded a result of type ‘String’ > Suggested fix: Suppress this warning by saying ‘_ <- string "("’ > | > 319 | string "(" > | ^^^^^^^^^^ > > HmmImpl.hs:344:33: error: [-Wincomplete-uni-patterns, > -Werror=incomplete-uni-patterns] > Pattern match(es) are non-exhaustive > In a pattern binding: Patterns of type ‘[Proof]’ not matched: [] > | > 344 | newSubproofStack@(newSubproof:_) = > (meaning !! n) subproofStack > | > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > > HmmImpl.hs:400:17: error: [-Wunused-do-bind, -Werror=unused-do-bind] > A do-notation statement discarded a result of type ‘String’ > Suggested fix: Suppress this warning by saying ‘_ <- string "$}"’ > | > 400 | string "$}" > | ^^^^^^^^^^^ > > HmmImpl.hs:410:33: error: [-Wunused-do-bind, -Werror=unused-do-bind] > A do-notation statement discarded a result of type ‘String’ > Suggested fix: > Suppress this warning by saying ‘_ <- string keyword’ > | > 410 | string keyword > | ^^^^^^^^^^^^^^ > > HmmImpl.hs:561:17: error: [-Wincomplete-uni-patterns, > -Werror=incomplete-uni-patterns] > Pattern match(es) are non-exhaustive > In a pattern binding: > Patterns of type ‘Statement’ not matched: > (_, _, DollarE) > (_, _, DollarF) > (_, _, (Axiom _ _)) > | > 561 | (_, expr, Theorem _ dvrSet proof) = stat > | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > make: *** [Makefile:9: hmmverify] Error 1 > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CAJ48g%2BCjdPZmvjLUGfu9xrC5Ggv6UgNVWsJz_dBez_DCAuxj-A%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAJ48g%2BCjdPZmvjLUGfu9xrC5Ggv6UgNVWsJz_dBez_DCAuxj-A%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuKBWA_HXK6UMjLhoUW5Hz%3D3Ayw6LrimGKMz2sKQB6KDg%40mail.gmail.com.
