Gaëtan Gilbert SkySkimmer
SkySkimmer
/ ivy-buffer-extend.el
Last active
October 15, 2017 12:38
— forked from frostidaho/ivy_buffer_extend.el
This file contains hidden or 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
| ;;; ivy-buffer-extend.el --- Extended display for ivy-switch-buffer -*- lexical-binding: t; -*- | |
| ;;; Original version https://gist.github.com/frostidaho/bc3a7b1be32f916dc65d no license included | |
| ;;; Changes by SkySkimmer licensed GPL3+ | |
| ;;; Commentary: | |
| ;; | |
| ;; This makes the interface to ivy-switch-buffer display mode and | |
| ;; location (backing file or default directory) for candidates in a | |
| ;; table, eg |
SkySkimmer
/ sig.txt
Created
October 24, 2017 21:26
This file contains hidden or 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
| sigma: Evd.evar_map = UNDEFINED EVARS: (+level 2 closure): | |
| ?X4==[ |- Type@{test.2}] (internal placeholder) {?T} | |
| ?X5==[ |- ?X4] (goal evar) {?Goal} | |
| ?X45==[ | |
| |- sig | |
| (forall _ : mix, | |
| sigT (sigT Prop (fun a : Prop => forall _ : nat, a)) | |
| (fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) => | |
| nat)) | |
| (fun |
SkySkimmer
/ foo
Created
December 1, 2017 13:31
This file contains hidden or 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
| -*- mode: compilation; default-directory: "~/dev/coq/coq/" -*- | |
| Compilation started at Fri Dec 1 14:27:18 | |
| make -C ~/dev/coq/coq/ analyze | |
| make: Entering directory '/home/gaetan/dev/coq/coq' | |
| make --warn-undefined-variable --no-builtin-rules -f Makefile.build analyze | |
| make[1]: Entering directory '/home/gaetan/dev/coq/coq' | |
| ECHO... > tools/tolink.ml | |
| OCAMLDEP tools/tolink.ml | |
| /home/gaetan/dev/dead_code_analyzer/build/dead_code_analyzer.opt -A -S -all config lib kernel intf kernel/byterun library engine pretyping interp proofs parsing printing tactics vernac stm toplevel tools tools/coqdoc plugins/omega plugins/romega plugins/micromega plugins/quote plugins/setoid_ring plugins/extraction plugins/fourier plugins/cc plugins/funind plugins/firstorder plugins/derive plugins/rtauto plugins/nsatz plugins/syntax plugins/btauto plugins/ssrmatching plugins/ltac plugins/ssr ide checker |
SkySkimmer
/ univs
Created
December 8, 2017 13:40
This file contains hidden or 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
| identity_rect_r.0 <= Coq.Init.Logic_Type.2 | |
| <= identity.0 | |
| identity_rec_r.0 <= Coq.Init.Logic_Type.2 | |
| <= identity.0 | |
| identity_ind_r.0 <= Coq.Init.Logic_Type.2 | |
| <= identity.0 | |
| Coq.Init.Logic_Type.2 <= identity.0 | |
| CompSpec2Type.0 <= CompSpecT.0 | |
| <= CompSpec.0 | |
| app.0 <= list.0 |
SkySkimmer
/ statuses.py
Last active
January 19, 2018 15:40
This file contains hidden or 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
| Python 3.6.4 (default, Jan 5 2018, 02:13:53) | |
| [GCC 7.2.0] on linux | |
| Type "help", "copyright", "credits" or "license" for more information. | |
| >>> python.el: native completion setup loaded | |
| >>> from github import Github | |
| >>> token = "REDACTED" | |
| >>> g = Github(token) | |
| >>> repo = g.get_repo("coq/coq") | |
| >>> pulls = repo.get_pulls() | |
| >>> pulls |
SkySkimmer
/ sprop.bench
Created
February 13, 2018 16:14
This file contains hidden or 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
| ┌──────────────────────────┬──────────────────────────┬──────────────────────────────────────┬────────────────────────────────────────┬─────────────────────────┬─────────────────┐ | |
| │ │ user time [s] │ CPU cycles │ CPU instructions │ max resident mem [KB] │ mem faults │ | |
| │ │ │ │ │ │ │ | |
| │ package_name │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ NEW OLD PDIFF │ | |
| ├──────────────────────────┼──────────────────────────┼──────────────────────────────────────┼────────────────────────────────────────┼─────────────────────────┼─────────────────┤ | |
| │ coq-flocq │ 59.28 59.35 -0.12 % │ 163160052594 162735358371 +0.26 % │ 210574808960 209452463755 |
SkySkimmer
/ gist:044906fd5884bb3f6cd1c3be28c9bfc8
Created
April 14, 2018 12:31
This file contains hidden or 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
| travis_fold:start:worker_info | |
| [0K[33;1mWorker information[0m | |
| hostname: 5d19dbcf-53f2-40ff-98de-4cfc02f4c834@1.production-4-worker-org-a-1-gce | |
| version: v3.6.0 https://github.com/travis-ci/worker/tree/170b2a0bb43234479fd1911ba9e4dbcc36dadfad | |
| instance: travis-job-edfa798e-8eab-424a-a589-57f0eff6a955 travis-ci-garnet-trusty-1512502259-986baf0 (via amqp) | |
| startup: 26.342739953s | |
| travis_fold:end:worker_info | |
| [0Kmode of ‘/usr/local/clang-5.0.0/bin’ changed from 0777 (rwxrwxrwx) to 0775 (rwxrwxr-x) | |
| travis_fold:start:system_info | |
| [0K[33;1mBuild system information[0m |
SkySkimmer
/ fooba
Created
April 20, 2018 14:46
This file contains hidden or 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
| ====== ill-typed term ==== | |
| application head= Cons((foo.equiv_inv),foo.106 foo.98 foo.99 foo.100) | |
| head type= | |
| (A:Type(foo.106)) | |
| (B:Type(foo.98)) | |
| (f:(#2->#2)) | |
| (IsEquiv:(Ind((foo.IsEquiv),0,foo.106 foo.98 foo.99 foo.100) #3#2#1)) | |
| (#3->#5) | |
| arguments: | |
| arg 1= (Ind((foo.paths),0,foo.105 foo.106) Type(foo.108)#3#2) |
SkySkimmer
/ foo.v
Created
April 20, 2018 14:47
This file contains hidden or 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
| (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *) | |
| Require Import Coq.Init.Notations. | |
| Global Set Universe Polymorphism. | |
| Notation "A -> B" := (forall (_ : A), B) : type_scope. | |
| Reserved Notation "A <~> B" (at level 85). | |
| Reserved Notation "f ^-1" (at level 3, format "f '^-1'"). |
SkySkimmer
/ baz
Created
April 26, 2018 13:40
This file contains hidden or 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
| HomologicalAlgebra/KATriangulated.v.html 193 28.855 34.683 5.828 | |
| HomologicalAlgebra/KATriangulated.v.html 96 20.092 24.157 4.065 | |
| HomologicalAlgebra/KA.v.html 475 23.398 26.484 3.086 | |
| Ktheory/GroupAction.v.html 373 27.376 30.397 3.021 | |
| HomologicalAlgebra/KA.v.html 453 13.395 15.166 1.771 | |
| CategoryTheory/LocalizingClass.v.html 1025 29.262 30.844 1.582 | |
| HomologicalAlgebra/KAPreTriangulated.v.html 444 6.235 7.308 1.073 | |
| HomologicalAlgebra/TranslationFunctors.v.html 1353 7.909 8.868 .959 | |
| HomologicalAlgebra/KAPreTriangulated.v.html 617 7.76 8.708 .948 | |
| HomologicalAlgebra/TranslationFunctors.v.html 1135 7.9 8.838 .938 |