Re: [Metamath] Help building hmm (Haskell Metamath verifier)

2024-03-19 Thread Antony Bartlett
On Mon, Mar 18, 2024 at 9:10 PM Mario Carneiro wrote: > On Mon, Mar 18, 2024 at 4:59 PM Antony Bartlett 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

Re: [Metamath] Help building hmm (Haskell Metamath verifier)

2024-03-18 Thread Mario Carneiro
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 wrote: > I've been trying to add hmm to metamath-docker, because

Re: [Metamath] Help building hmm (Haskell Metamath verifier)

2024-03-18 Thread Mario Carneiro
On Mon, Mar 18, 2024 at 4:59 PM Antony Bartlett 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] Help building hmm (Haskell Metamath verifier)

2024-03-18 Thread Antony Bartlett
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