basetunnel

cabal-dev ghci error

1

When running cabal-dev ghci on a cabal library project that has no source code (or does not export any modules) the following error message appears: ``` $cabal-dev ghci FAILED: Failed...

Implement dumping a compilation trace of the pir-pir pipeline for the Coq certifier

3

This PR adds dumping of all intermediate PIR ASTs (the "compilation trace"), in a format that can be handled on the Coq side for the certifier. It adds the types...

Many links broken on http://mattam82.github.io/Coq-Equations/

1

Since `master` was renamed to `main`, many links broke on the website, for example to the user guide. It is fixed in the README of the repo, and it seems...

Fix for deriving DecOpt when index of inductive is from an inductive family

3

This is the same fix as in https://github.com/QuickChick/QuickChick/pull/314 but applied on `master` (and I squashed the two commits that introduced changes). Please see that PR for more details.

I tried to install with the instructions, but got the following error using stack 2.9.1: ``` jacco@betal082367:~/sources/hs-to-coq$ stack clean jacco@betal082367:~/sources/hs-to-coq$ stack build ghc: panic! (the 'impossible' happened) (GHC version 8.4.3...

Typechecked Insertion combinators generate invalid query

1

This code compiles: ```haskell {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE...

Add flag to dump PIR ASTs for certifier

7

Context --- For my certifier in Coq, I need to get my hands on all intermediate PIR ASTs. I've added a plugin flag `dump-cert-trace`, that dumps all PIR ASTs to...