On Mon, Mar 18, 2024 at 9:10 PM Mario Carneiro <[email protected]> wrote:
> On Mon, Mar 18, 2024 at 4:59 PM Antony Bartlett <[email protected]> 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 <[email protected]> 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 -- 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%2BC1wtzSMDzGnGNKRn6aFTHvi1FMLvoy%2B4CgForGWek9eA%40mail.gmail.com.
