Skip to content

Instantly share code, notes, and snippets.

🐫
🐫.P(🐫) → ∅ ≡ (∃🐫.P(🐫)) → ∅

Yuriy Pitomets Pitometsu

🐫
🐫.P(🐫) → ∅ ≡ (∃🐫.P(🐫)) → ∅
  • Ukraine
Block or report user

Report or block Pitometsu

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@Pitometsu
Pitometsu / even.ml
Last active Dec 1, 2019
Even: Coq to OCaml
View even.ml
type _ num =
| Zero : zero num
| Succ : ('a num) -> 'a plus num
and _ plus = Plus : 'a num -> 'a plus
and zero = [ ]
;;
type _ even =
| Even_0 : zero num even
| Even_S : 'a num odd -> 'a plus num even
and _ odd =
@Pitometsu
Pitometsu / shell.nix
Created Nov 27, 2019
Coq environment
View shell.nix
let
overlays = [
(self: super: with self; {
coq = coq_8_10;
coq_8_10 = (super.coq_8_10.override { buildIde = false; });
coqPackages = coqPackages_8_10;
coqPackages_8_10 = (super.coqPackages_8_10.overrideScope' (self: super: {
inherit coq;
}));
})
View macos-ld-fix.nix
macos-ld-fix = stdenv.mkDerivation {
name = "macos-ld-fix";
src = null;
unpackPhase = "true";
dontBuild = true;
installPhase = ''
mkdir -p $out/opt/local/lib
'';
};
View functors.ml
module type M = sig
module type S
module S : S
end
;; module type M = sig module type S module S : S end
@Pitometsu
Pitometsu / cc.nix
Created Sep 24, 2019
Nix overlay to override system compiler
View cc.nix
(self: super:
let
stdenv = let stdenv = super.overrideCC super.stdenv super.gcc8; in
stdenv.override { cc = super.stdenv.cc; };
in {
inherit stdenv;
})
# stdenv = gcc8Stdenv.override {
# cc = gcc8Stdenv.override {
# inherit (self) libc;
@Pitometsu
Pitometsu / example.ml
Created Sep 19, 2019
Can module-level have Upper Type Bounds
View example.ml
utop#
module type T = sig
type t = ..
end;;
module type T = sig type t = .. end
utop #
@Pitometsu
Pitometsu / wtf.sh
Created Sep 18, 2019
Darwin stdlib problem
View wtf.sh
$ nix-shell -p gcc8 --command 'echo $NIX_CFLAGS_COMPILE'
-isystem /nix/store/aj932q5vd2xzl67v3qs6hsg47lxmf0n2-libc++-5.0.2/include -isystem /nix/store/89gnz8abjwra67d8y6s6ysmjl6ji81ai-libc++abi-5.0.2/include -isystem /nix/store/yr2vwrbjgabcskp153nzsyl72ysbfc1g-compiler-rt-5.0.2-dev/include -F/nix/store/7x42k0scp8xscrf092jalvpns4cwnnj3-swift-corefoundation/Library/Frameworks -isystem /nix/store/aj932q5vd2xzl67v3qs6hsg47lxmf0n2-libc++-5.0.2/include -isystem /nix/store/89gnz8abjwra67d8y6s6ysmjl6ji81ai-libc++abi-5.0.2/include -isystem /nix/store/yr2vwrbjgabcskp153nzsyl72ysbfc1g-compiler-rt-5.0.2-dev/include -F/nix/store/7x42k0scp8xscrf092jalvpns4cwnnj3-swift-corefoundation/Library/Frameworks
@Pitometsu
Pitometsu / cc-overlay.nix
Created Sep 13, 2019
How to override CC by Nix overlay?
View cc-overlay.nix
(self: super:
let
# gcc = super.pkgs.gcc8;
# gcc8 = super.pkgs.gcc8.override { stdenv = super.stdenv; };
stdenv = super.stdenvAdapters.overrideCC super.stdenv super.pkgs.gcc8;
in
{
inherit stdenv; # gcc8 gcc;
# stdenv = super.overrideCC super.stdenv self.pkgs.gcc;
# gcc8 = super.gcc8.override { stdenv = super.stdenv; };
@Pitometsu
Pitometsu / m.ml
Created Aug 21, 2019
first-class modules type limitation
View m.ml
utop # let (module M) = (module Caml.Map.Make(Int64) : Caml.Map.S) in let to_ : unit -> _ M.t = fun () -> failwith "und" in to_;;
Error: This expression has type unit -> 'a M.t
but an expression was expected of type 'b
The type constructor M.t would escape its scope
utop # let module M = Caml.Map.Make(Int64) in let to_ : unit -> _ M.t = fun () -> failwith "und" in to_;;
- : unit -> 'a Map.Make(Core_kernel__Int64).t = <fun>
You can’t perform that action at this time.