Haskell 使用 GHC 为 Paradox 定理证明器制作配方失败

Question

我正在尝试安装源自 here 的悖论定理证明器。

当我运行生成文件时，这是运行的命令： ghc -optl -static -lstdc++ -I../instantiate -I../minisat/current-base ../minisat/current-base/Solver.or ../minisat/current-base/Prop.or ../instantiate/MiniSatWrapper.or ../instantiate/MiniSatInstantiateClause.or -fglasgow-exts -O2 -static -threaded -main-is Paradox.Main.main --make Paradox.Main -o paradox

它会导致几个错误，如下所示：

Flags.hs:52:8:
    Could not find module ‘Char’
    Use -v to see a list of the files searched for.

适用于各种模块，包括但不限于 Char、CPUTime、IO。

最后的错误信息是

Makefile:38: recipe for target 'paradox.exe' failed
make: *** [paradox.exe] Error 1

我不知道 Haskell，我对 GNU 也不是很有经验 make，但我正在尝试为一个项目安装这个包，但它不够晦涩，无法打包我的 OS（我是运行ning Arch Linux）。据我所知，它没有为任何 OS 打包，因此需要从源安装。

据我所知，问题始于以下错误消息：

on the commandline: Warning: -fglasgow-exts is deprecated: Use individual extensions instead

我正在使用 Arch Linux 软件包存储库中提供的 GHC 版本：package link

Answer 1

看起来悖论是为相当旧的 GHC 版本编写的。您可以使用 GHC 7.8 或更早版本并设置

来修复所有这些 "Could not find module" 错误

GHC     = ghc -hide-package base -package haskell98

在 Makefile 中，尽管之后您可能会遇到更多错误。

关于-fglasgow-exts的警告大多是无害的，你可以忽略它。

Haskell 使用 GHC 为 Paradox 定理证明器制作配方失败

Haskell make recipe fails for Paradox theorem prover using GHC

linux

haskell

makefile

ghc

theorem-proving