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.
