chrbur02$ cd base C02TD0UUHF1T:base chrbur02$ make clean CLEAN C02TD0UUHF1T:base chrbur02$ cd .. C02TD0UUHF1T:hs-to-coq chrbur02$ cd base-thy C02TD0UUHF1T:base-thy chrbur02$ make clean CLEAN C02TD0UUHF1T:base-thy chrbur02$ cd .. C02TD0UUHF1T:hs-to-coq chrbur02$ make -C base COQDEP VFILES COQC GHC/Wf.v COQC GHC/Types.v COQC GHC/Prim.v COQC GHC/Tuple.v COQC GHC/Num.v File "./GHC/Num.v", line 89, characters 0-22: Warning: Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one. [require-in-module,deprecated] COQC GHC/Char.v COQC GHC/Base.v File "./GHC/Base.v", line 550, characters 0-21: Warning: Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one. [require-in-module,deprecated] COQC GHC/Skip.v COQC GHC/Err.v COQC GHC/DeferredFix.v COQC GHC/DeferredFixImpl.v COQC GHC/List.v COQC GHC/Enum.v COQC GHC/Real.v COQC Data/Maybe.v COQC Data/Bits.v COQC Data/Type/Equality.v COQC GHC/Nat.v COQC GHC/Unicode.v COQC Data/Monoid.v COQC Data/Either.v COQC Data/Proxy.v COQC Data/SemigroupInternal.v COQC Data/Foldable.v COQC Data/Functor.v COQC Data/Functor/Const.v COQC Data/Functor/Identity.v COQC Data/Functor/Utils.v COQC Data/Traversable.v COQC Control/Monad.v COQC Data/Tuple.v COQC Prelude.v COQC Data/List.v COQC Data/Ord.v COQC Data/OldList.v COQC Data/Bool.v COQC Data/Void.v COQC Data/Function.v COQC Control/Monad/Fail.v COQC Control/Category.v COQC Control/Arrow.v COQC Control/Applicative.v COQC Data/Functor/Classes.v COQC Data/Bifunctor.v COQC Data/List/NonEmpty.v COQC Data/Bifoldable.v COQC Data/Bitraversable.v COQC Data/Semigroup.v COQC Data/Functor/Compose.v COQC Control/Monad/Zip.v COQC Data/Functor/Product.v COQC Data/Functor/Sum.v C02TD0UUHF1T:hs-to-coq chrbur02$ make -C base-thy COQDEP VFILES COQC GHC/Base.v File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. File "./GHC/Base.v", line 411, characters 7-29: Warning: Nothing to inject. COQC Data/Either.v File "./Data/Either.v", line 5, characters 0-31: Warning: Trying to mask the absolute name "GHC.Base"! [masking-absolute-name,deprecated] COQC GHC/List.v File "./GHC/List.v", line 8, characters 0-31: Warning: Trying to mask the absolute name "GHC.Base"! [masking-absolute-name,deprecated] COQC Data/Foldable.v File "./Data/Foldable.v", line 4, characters 0-31: Warning: Trying to mask the absolute name "GHC.Base"! [masking-absolute-name,deprecated] File "./Data/Foldable.v", line 5, characters 0-31: Warning: Trying to mask the absolute name "GHC.List"! [masking-absolute-name,deprecated] COQC Data/Traversable.v File "./Data/Traversable.v", line 4, characters 0-31: Warning: Trying to mask the absolute name "GHC.Base"! [masking-absolute-name,deprecated] File "./Data/Traversable.v", line 5, characters 0-31: Warning: Trying to mask the absolute name "GHC.List"! [masking-absolute-name,deprecated] COQC Data/Functor/Classes.v File "./Data/Functor/Classes.v", line 4, characters 0-31: Warning: Trying to mask the absolute name "GHC.Base"! [masking-absolute-name,deprecated] COQC Data/OldList.v COQC Data/Ord.v File "./Data/Ord.v", line 2, characters 0-31: Warning: Trying to mask the absolute name "GHC.Base"! [masking-absolute-name,deprecated] COQC Data/Proxy.v File "./Data/Proxy.v", line 2, characters 0-31: Warning: Trying to mask the absolute name "GHC.Base"! [masking-absolute-name,deprecated] COQC Data/Tuple.v COQC GHC/Enum.v COQC Termination.v File "./Termination.v", line 4, characters 0-31: Warning: Trying to mask the absolute name "GHC.Base"! [masking-absolute-name,deprecated] COQC Data/Bits/Popcount.v COQC Prelude.v File "./Prelude.v", line 1, characters 0-31: Warning: Trying to mask the absolute name "GHC.Base"! [masking-absolute-name,deprecated] File "./Prelude.v", line 2, characters 0-31: Warning: Trying to mask the absolute name "GHC.List"! [masking-absolute-name,deprecated] File "./Prelude.v", line 3, characters 0-31: Warning: Trying to mask the absolute name "GHC.Enum"! [masking-absolute-name,deprecated] File "./Prelude.v", line 6, characters 0-34: Warning: Trying to mask the absolute name "Data.Either"! [masking-absolute-name,deprecated] File "./Prelude.v", line 7, characters 0-36: Warning: Trying to mask the absolute name "Data.Foldable"! [masking-absolute-name,deprecated] File "./Prelude.v", line 8, characters 0-35: Warning: Trying to mask the absolute name "Data.OldList"! [masking-absolute-name,deprecated] File "./Prelude.v", line 9, characters 0-31: Warning: Trying to mask the absolute name "Data.Ord"! [masking-absolute-name,deprecated] File "./Prelude.v", line 10, characters 0-33: Warning: Trying to mask the absolute name "Data.Proxy"! [masking-absolute-name,deprecated] File "./Prelude.v", line 11, characters 0-39: Warning: Trying to mask the absolute name "Data.Traversable"! [masking-absolute-name,deprecated] File "./Prelude.v", line 12, characters 0-33: Warning: Trying to mask the absolute name "Data.Tuple"! [masking-absolute-name,deprecated] C02TD0UUHF1T:hs-to-coq chrbur02$ ls LICENSE cabal.project hs-to-coq.cabal Main.glob common.mk notes Main.h2ci core-semantics-no-values readthedocs.yml Main.v count-failures.pl src README.md default.nix stack.yaml Setup.hs dir-locals.nix stack.yaml.lock Transp.hs doc structural-isomorphism-plugin base emacs base-thy examples C02TD0UUHF1T:hs-to-coq chrbur02$ cd examples/ C02TD0UUHF1T:examples chrbur02$ ls bag coinduction dlist lambda shuffle transformers base-src compiler ghc quicksort simple wc base-tests containers graph resources successors boot.sh core-semantics intervals rle tests C02TD0UUHF1T:examples chrbur02$ cd bag C02TD0UUHF1T:bag chrbur02$ coqtop -l Bag.v Welcome to Coq 8.10.0 (February 2020) File "/Users/chrbur02/Coq/hs-to-coq/examples/bag/Bag.v", line 12, characters 15-23: Error: Cannot find a physical path bound to logical path matching suffix GHC.