Dennis Gosnell cdepillabout
cdepillabout
/ set-proof-example.idr
Created
December 4, 2018 04:00
Some proofs of simple things from set theory, including how to define power sets and subsets. All in Idris.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module Set2 | |
| -- | |
| -- This module has some proofs of things from set theory. Inspired by | |
| -- chapter 13 of the book Type Theory and Formal Proofs. | |
| -- | |
| -- A power set of some given set s. | |
| PowerSet : (s : Type) -> Type | |
| PowerSet s = s -> Type |
cdepillabout
/ cudatoolkit-release-18.09-and-19.03.diff
Created
March 20, 2019 03:14
Git diff between cudatoolkit derivation from release-18.09 and release-19.03 branch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $ git diff release-18.09 release-19.03 -- pkgs/development/compilers/cudatoolkit/default.nix | |
| diff --git a/pkgs/development/compilers/cudatoolkit/default.nix b/pkgs/development/compilers/cudatoolkit/default.nix | |
| index e44c21abe94..3a34d14f8ad 100644 | |
| --- a/pkgs/development/compilers/cudatoolkit/default.nix | |
| +++ b/pkgs/development/compilers/cudatoolkit/default.nix | |
| @@ -1,6 +1,6 @@ | |
| -{ lib, stdenv, makeWrapper, fetchurl, requireFile, perl, ncurses, expat, python27, zlib | |
| -, gcc48, gcc49, gcc5, gcc6 | |
| -, xorg, gtk2, glib, fontconfig, freetype, unixODBC, alsaLib, glibc | |
| +{ lib, stdenv, makeWrapper, fetchurl, requireFile, perl, ncurses5, expat, python27, zlib |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE InstanceSigs #-} | |
| module MaybeT where | |
| import Control.Monad.Trans | |
| newtype MaybeT m a = MaybeT { unMaybeT :: m (Maybe a) } | |
| instance MonadTrans MaybeT where | |
| lift :: Monad m => m a -> MaybeT m a |
cdepillabout
/ example.hs
Created
April 11, 2019 02:08
show how quantifiedconstraints can be used for writing highly polymorphic versions of functions like pure
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE FlexibleContexts #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE InstanceSigs #-} | |
| {-# LANGUAGE QuantifiedConstraints #-} | |
| {-# LANGUAGE RoleAnnotations #-} | |
| {-# LANGUAGE TypeApplications #-} | |
| {-# OPTIONS_GHC -Wall #-} | |
| module MaybeT where |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| with (import ~/git/nixpkgs {}); | |
| let | |
| libs = [ | |
| alsaLib | |
| at-spi2-atk | |
| atk | |
| cairo | |
| cups | |
| dbus |
cdepillabout
/ dependently-typed-tensor.hs
Created
May 30, 2019 17:01
A half-working dependently typed tensor library based on the linear package
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE DefaultSignatures #-} | |
| {-# LANGUAGE DerivingStrategies #-} | |
| {-# LANGUAGE EmptyCase #-} | |
| {-# LANGUAGE ExistentialQuantification #-} | |
| {-# LANGUAGE FlexibleContexts #-} | |
| {-# LANGUAGE FlexibleInstances #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE InstanceSigs #-} | |
| {-# LANGUAGE KindSignatures #-} |
cdepillabout
/ cabal-install-output-with-error.txt
Last active
July 3, 2019 11:13
https://github.com/haskell/cabal/issues/6125
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $ cabal new-install exe:ormolu -v3 | |
| File monitor 'config' unchanged. | |
| this build was affected by the following (project) config files: | |
| - /home/illabout/git/ormolu/cabal.project.local | |
| Reading available packages of hackage.haskell.org... | |
| Using most recent state (could not read timestamp file) | |
| Warning: The package list for 'hackage.haskell.org' does not exist. Run 'cabal | |
| update' to download it. | |
| index-state(hackage.haskell.org) = | |
| File monitor 'improved-plan' unchanged. |
cdepillabout
/ example.nix
Last active
February 7, 2023 03:52
Example of overriding a GHC core Haskell package with Nix
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # This file is an example of overriding a GHC core Haskell library (like | |
| # bytestring, containers, text, unix, etc) when building a Haskell package. | |
| let default-nixpkgs = | |
| builtins.fetchTarball { | |
| # nixpkgs haskell-updates branch as of 2019/09/15. | |
| url = "https://github.com/NixOS/nixpkgs/archive/a51b3367ab6acc72630da0bad50ce14fa86996d0.tar.gz"; | |
| sha256 = "05d3jxxk5dxzs9b3nan16lhkrjnzf0bjd4xy66az86fsafnrr9rd"; | |
| }; | |
| in |
cdepillabout
/ purescript-build-output-err-haddock.txt
Last active
November 6, 2019 10:19
Error when building purescript with --haddock option to stack
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Building library for purescript-0.13.4.. | |
| [ 1 of 163] Compiling Control.Monad.Logger | |
| [ 2 of 163] Compiling Control.Monad.Supply | |
| [ 3 of 163] Compiling Control.Monad.Supply.Class | |
| [ 4 of 163] Compiling Language.PureScript.Comments | |
| [ 5 of 163] Compiling Language.PureScript.AST.SourcePos | |
| [ 6 of 163] Compiling Language.PureScript.Crash | |
| [ 7 of 163] Compiling Language.PureScript.AST.Operators | |
| [ 8 of 163] Compiling Language.PureScript.Docs.Css | |
| [ 9 of 163] Compiling Language.PureScript.Docs.Utils.MonoidExtras |
cdepillabout
/ juggling-data
Last active
March 14, 2020 16:08
Days practicing 5 minutes of juggling, and days new records were set
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Index,Date,NewRecord | |
| 0,2019-06-23 | |
| 1,2019-06-24 | |
| 2,2019-06-25 | |
| 3,2019-06-26 | |
| 4,2019-06-27 | |
| 5,2019-06-28 | |
| 6,2019-06-29 | |
| 7,2019-06-30 | |
| 8,2019-07-01 |