在我的项目中,我有几个QuickCheck属性,其中大部分是我使用forAllProperties收集的,在Test.QuickCheck.All中定义.我试图并行运行我的所有属性,这很麻烦:在运行结束时,我得到了在终端中打印的输出,并且反例和属性名称经常被分散,以致难以将属性与其计数器匹配例子.
我看到库pqc的目的是并行运行属性,但它不提供forAllProperties的替代,也没有提供将forAllProperties与并行测试驱动程序组合的方法.
感觉就像我需要的是forAllProperties将属性名称传递给它作为参数获取的函数.
我还研究了在线程基础上重定向stdout,首先使用system-posix-redirect(这不是线程安全的),然后研究Test.QuickCheck.State,尤其是终端字段.后者没有成功,因为我没有找到重写终端字段的方法.
有没有办法让我以某种方式输出反例和属性名称,而无需复制/粘贴Test.QuickCheck.All模块并进行我需要的更改？
我正在使用精益定理证明器,我想构建类似堆栈的功能并开始构建库缓存.我不确定的一件事是何时删除缓存中的旧包.我可以认为,如果我安装了两个版本的Lean,比如3.3.0和3.3.1,我可以争辩保留所有适用于这些版本的软件包的所有版本.由于精益语法移动速度很快,因此限制性很强.
另一方面,我可以看到只保留任何给定包的10个版本.这可能是10个最新版本或10个最近请求的版本.
我很想知道在构建stack和相关工具中考虑的一些想法.
考虑以下 Haskell 代码：
import Data.Coerce
newtype Decorated s a = Decorated a
fancyFunction :: Ctx s => f (Decorated s a) -> r
fancyFunction = ...
instance Ctx s => SomeClass (Decorated s a)
myFunction :: Functor f => f a -> r
myFunction = fancyFunction . fmap coerce
我想提出myFunction通过更换速度更快fmap coerce用coerce。其基本原理是 ，coerce其行为类似于id并且函子定律之一是fmap id = id。
我可以看到这样做的唯一方法是添加Coercible (f a) (f (Decorated s a))到上下文中，但它指的是 s 没有在其他任何地方被引用。更糟糕的是，如果a绑定在通用类型中，我无法表达约束。有没有我可以表达的限制， …
我正在HaTeX之上构建一个eDSL.我面临的问题是我想在我的LaTeX文档中显示Haskell表达式,并且我想使用相同的Haskell表达式来帮助生成文档.
显而易见的答案是复制并粘贴表达式,使其显示为引用和实时.我想避免这种情况,因为表达式可能会发生变化.
我想象的是一个准引号,它既可以拼接其内容,也可以输出代表它的字符串.
例如,以下是我要输入的内容:
document = do
title "this is an example document"
paragraph "This is normal text. We will now show the Haskell code that generates a table"
[quoted| makeTable ["heading1","heading2"] ["cell1","cell2"] |]
我希望准引言扩展到:
document = do
title "this is an example document"
paragraph "This is normal text. We will now show the Haskell code that generates a table"
makeTable ["heading1","heading2"] ["cell1","cell2"]
listing Haskell "makeTable [\"heading1\",\"heading2\"] [\"cell1\",\"cell2\"]"
为此,我需要编写一个QuasiQuoter:
quoted :: QuasiQuoter
quoted = QuasiQuoter
{ quoteExp = \str -> …我有两个文件,其内容相同,除了我放置断言的顺序:在一个文件中,断言按照另一个的相反顺序放置.第一个文件(po-9.z3)在不到一秒的时间内被Z3声明为不可用,而另一个(po.z3)在一分钟内无法验证.
造成这种差异的原因是什么？我假设将先前在验证中涉及的断言放在文件中会改善性能.但是,通过验证的那个(po-9.z3)在文件的底部有大多数相关/特定于问题的断言.另外,在po.z3中,虽然要证明的定理和假设位于文件的顶部,但是一个重要的断言(lambda表达式的一阶公式)放在文件的底部.当我把它带到顶部时,po.z3会在不到一秒的时间内完成验证.
在z3 smt2文件中生成断言的最佳顺序是什么？