Help building hmm (Haskell Metamath verifier)
37 views
Skip to first unread message
Antony Bartlett
Mar 18, 2024, 4:59:52 PMMar 18
to meta...@googlegroups.com
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 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
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
Mario Carneiro
Mar 18, 2024, 5:10:17 PMMar 18
to meta...@googlegroups.com
On Mon, Mar 18, 2024 at 4:59 PM Antony Bartlett <a...@akb.me.uk> wrote:
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
As a docker noob, could you explain to me how containerization helps with this in any way? You still have to have all those things, plus docker, if you are doing it with containers.
Mario Carneiro
Mar 18, 2024, 5:12:39 PMMar 18
to meta...@googlegroups.com
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 <a...@akb.me.uk> wrote:
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJ48g%2BCjdPZmvjLUGfu9xrC5Ggv6UgNVWsJz_dBez_DCAuxj-A%40mail.gmail.com.
Antony Bartlett
Mar 19, 2024, 6:08:02 AMMar 19
to meta...@googlegroups.com
On Mon, Mar 18, 2024 at 9:10 PM Mario Carneiro <di....@gmail.com> wrote:
On Mon, Mar 18, 2024 at 4:59 PM Antony Bartlett <a...@akb.me.uk> wrote: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
As a docker noob, could you explain to me how containerization helps with this in any way? You still have to have all those things, plus docker, if you are doing it with containers.
Well, I have all those things in a container, so the Dockerfile just builds. I've automated three different builds in different programming languages, and they should always work because they're always built within the same container. Or if they don't work - to give a real example - because metamath.exe's source files have been moved from the root of metamath.zip to a src directory, then I know immediately I haven't done anything wrong and can look at what's changed in metamath.exe and make the matching adjustment to the Dockerfile. The "well it works on my machine" frustration is as good as eliminated by this approach.
No one else has to build this docker container if they don't wish to, they can just pull the docker image which I've pushed to dockerhub. That's the biggest advantage - it provides an environment which is the same for everyone. When I came back to this project after two years I was on a completely different laptop, might even have changed OS, but it didn't matter because it was still the same docker container.
And hopefully I can get this Haskell build working too and then never have to worry about it again.
On Mon, Mar 18, 2024 at 9:12 PM Mario Carneiro <di....@gmail.com> wrote:
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.
I haven't turned anything off or on, and if I had then the Dockerfile would make that explicit - you don't need to ask if I've done something silly because you can just check. I mean, I do silly things all the time, it's just that it should be transparent in this context ;-). Looking for a setting I can explicitly turn off in order to make this build succeed is a great idea, however, and I will investigate that as soon as I get the chance. Thank you very much for your advice,
Best regards,
Antony
Reply all
Reply to author
Forward
0 new messages