Closed EricGT closed 2 years ago
nomeata
commented
2 years ago As you can tell, this project is quite old. At this point, I probably not only have to update the build instructions, but renovate the way this is built completely, so a larger project.
But yes, it’s probably worth fighting the bitrot…
EricGT
commented
2 years ago Thanks.
I (GuyCoder) don't mind doing the leg work as I will learn something. I would need someone to point me in the right direction when I get stuck. I realize this is more than several hours of work and could take a few weeks to run through some combinations or get the pieces to fit together as needed.
This question was prompted by my question.
nomeata
commented
2 years ago Ah, you want to import metamath proofs into the Incredible Proof Machine? Fun idea…
So far I have only thought about the other direction – generating human readable proofs, or Isabelle proofs etc. from Incredible Proof Machine proofs.
It seems that one requirement is to have an interchange format for proofs in the Incredible Proof Machine that you could target in such a tool.
nileshtrivedi
commented
2 years ago +1 for updating build instructions. Here are the things I have tried and failed:
asdf's haskell plugin on M1 mac to install ghc v7.10.3 but ran into this issue and could not install cabal. extra-deps, but that led to another error: network library uses unknwon extension TypeApplications. Moreover, network doesn't support GHC 7.x anymore.hvr/ghc ppa, I was unable to install ghc:
nileshtrivedi
commented
2 years ago I was able to get cabal v2.4.1.0 working with the following:
asdf install haskell 8.6.5
asdf global haskell 8.6.5
asdf reshim
stack install cabal-install --resolver lts-14.27Then cabal install http://ghcjs.luite.com/master-20151222.tar.gz ghcjs-boot --no-prof gave the error:
cabal: unrecognized 'install' option `--no-prof'Removing the --no-prof option led to this error:
Warning: The install command is a part of the legacy v1 style of cabal usage.
Please switch to using either the new project style and the new-install
command or the legacy v1-install alias as new-style projects will become the
default in the next version of cabal-install. Please file a bug if you cannot
replicate a working v1- use case with the new-style commands.
For more information, see: https://wiki.haskell.org/Cabal/NewBuild
Downloading http://ghcjs.luite.com/master-20151222.tar.gz
<socket: 15>: hGetBufSome: timeout (Operation timed out)Because http://ghcjs.luite.com/ does not resolve any more.
nomeata
commented
2 years ago Yes, it's a mess. I worked on it a bit two weeks ago, and it took me a while to even compile it again. Also the CI systis broken and I had to manually deploy.
I need to redo the whole build setup, probably using nix, which will make it easier for others to get a working ghcjs etc.
nileshtrivedi
commented
2 years ago @nomeata Did you get a chance to revisit the build instructions? Is there a way I can help?
nomeata
commented
2 years ago I worked a bit on it in July, but dropped the ball again. I’m inclined to build the build system on nix, working with GHCJS is much easier there. Have you worked with nix before?
I pushed the beginnings of my work there to shell.nix on branch nixify. I believe running make in a nix-shell should work already! (It will probably build ghcjs and a bunch of things the first time, so better run it over night or something like that.)
nileshtrivedi
commented
2 years ago No, I'm in the same boat as @EricGT - never built anything with Haskell toolchain (or nix).
EricGT
commented
2 years ago @nileshtrivedi Nice to see others in the same boat. FYI my being able to build Incredible Proof Machine so I can add custom logics is no longer high enough on my list that I can actively work toward that end in the foreseeable future. If it becomes easy to build from source and then add a custom logic in a days time I might give it a try but for now I just keep tabs on this from afar.
nomeata
commented
2 years ago If you just need to add logics then I'm theory you should not need to build to code, just edit files https://github.com/nomeata/incredible/tree/master/logics.
But right now I am converting these files to JSON and concatenate them, using a tool written in Haskell…
Anyways, using nix isn't hard, so the above should work
nomeata
commented
2 years ago Ok, as of d3ee8b1e5dca0bd6e2bd09ff59d803b964a5da75 the build instruction in the README are updated to use nix, and we now have a CI/CD system again (using Github actions).
nileshtrivedi
commented
2 years ago I can confirm that I was able to build incredible on Apple M1 with the new Nix-based setup (although the nix-build command took more than 4 hours - even with Kaleidogen cache)! Thanks @nomeata 👏 🎉 😄
nomeata
commented
2 years ago Ah, yes, the cache will only have Linux artifacts. Thanks for persevering!
EricGT
commented
2 years ago It seems that others have taken notice of this and noted IPM on Hacker News (https://news.ycombinator.com/).
I have never built using a Haskell toolchain before so following the instructions.
Then this appears.
This is a great application and easy to use for learning Proofs. I don't know the Haskell toolchain but those that do I suspect could easily update the instructions and save others time and effort. While some are persistent and will try to figure this out, many will just walk away at this point.
Note: Please add the optional steps for installing the tools without having been installed before. In other words the instructions seem to imply the tools have been installed and just need to be updated, there are users like me who have never installed the Haskell toolchain.