Skip to content

Instantly share code, notes, and snippets.

Clément Pit-Claudel cpitclaudel

Block or report user

Report or block cpitclaudel

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
View 0001-doc-Add-position-information-to-messages-printed-whe.patch
From 1815f38d4b41257b02c08fa73d50f64712a801a0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= <clement.pitclaudel@live.com>
Date: Thu, 7 Feb 2019 15:39:35 -0500
Subject: [PATCH] [doc] Add position information to messages printed when
coqtop fails
---
doc/tools/coqrst/coqdomain.py | 69 +++++++++++++++++++++++++----------------
doc/tools/coqrst/repl/coqtop.py | 22 ++++++++-----
2 files changed, 56 insertions(+), 35 deletions(-)
View bt
RangeError: Maximum call stack size exceeded
at head_matches
at aux
at head_matches_delta
at rigid_rigid_delta
at solve_t$0
at caml_trampoline
at solve
at rigid_rigid_delta
at solve_t$0
@cpitclaudel
cpitclaudel / fstar.core.byte
Last active Mar 26, 2018
js_of_ocaml output
View fstar.core.byte
This file has been truncated, but you can view the full file.
View gist:4de0ceaca4b280ef6d4b0965351dc044
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Exception of type 'System.InvalidProgramException' was thrown.
* Assertion at metadata.c:939, condition `index < meta->heap_strings.size' not met
Stacktrace:
at <unknown> <0xffffffff>
at (wrapper managed-to-native) System.RuntimeType.GetMethodsByName (System.RuntimeType,string,System.Reflection.BindingFlags,bool,System.Type) <0xffffffff>
at System.RuntimeType.GetMethodCandidates (string,System.Reflection.BindingFlags,System.Reflection.CallingConventions,System.Type[],bool) <0x0009c>
at System.RuntimeType.GetMethods (System.Reflection.BindingFlags) <0x00044>
@cpitclaudel
cpitclaudel / many-errors.py
Created Nov 23, 2016
Large python file full of errors
View many-errors.py
def a(x, y, y):
return t; pass
def a(x, y, y):
return t; pass
def a(x, y, y):
return t; pass
def a(x, y, y):
return t; pass
def a(x, y, y):
return t; pass
View gist:a945495964bd89f15cc1d20b356d43a3
[profiler-profile "24.3" cpu #s(hash-table size 1095 test equal rehash-size 1.5 rehash-threshold 0.8 data ([puthash "#<compiled 0xb4de2f9>" maphash profiler-calltree-build-unified profiler-calltree-build profiler-report-render-calltree-1 profiler-report-rerender-calltree profiler-report-render-calltree profiler-report-setup-buffer profiler-report-profile-other-window profiler-report-cpu profiler-report funcall-interactively "#<subr call-interactively>" ad-Advice-call-interactively apply] 4 [maphash profiler-calltree-build-unified profiler-calltree-build profiler-report-render-calltree-1 profiler-report-rerender-calltree profiler-report-render-calltree profiler-report-setup-buffer profiler-report-profile-other-window profiler-report-cpu profiler-report funcall-interactively "#<subr call-interactively>" ad-Advice-call-interactively apply call-interactively command-execute] 228 ["#<compiled 0xb4de2f9>" maphash profiler-calltree-build-unified profiler-calltree-build profiler-report-render-calltree-1 profiler-repo
@cpitclaudel
cpitclaudel / mindless-extraction.el
Last active Dec 26, 2015
Experiments with real-time extraction
View mindless-extraction.el
(require 'dash)
(defun company-coq--plug-subproof-holes (partial-proof)
"Plug evars in PARTIAL-PROOF, producing a closed term.
Note that type inference may fail on that term."
(replace-regexp-in-string (concat "[?]\\(" coq-id "\\(@{[^}]+}\\)?\\)")
"(_UNFINISHED_GOAL_ _)"
partial-proof t))
(defun company-coq-backto (state)
View pg-plugin.el
(defun my-pg-preprocessor (coq-sentence)
"Run COQ-SENTENCE through preprocessor and return the result."
(let ((preprocessor (with-current-buffer proof-script-buffer
(expand-file-name "./preprocessor.rb"))))
(with-temp-buffer
(insert coq-sentence)
(call-process-region (point-min) (point-max) preprocessor t '(t nil) nil)
(buffer-string))))
(defun my-pg-preprocessor-hook ()
You can’t perform that action at this time.