Skip to content

Instantly share code, notes, and snippets.

View cpitclaudel's full-sized avatar

Clément Pit-Claudel cpitclaudel

View GitHub Profile
(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 ()
@cpitclaudel
cpitclaudel / mindless-extraction.el
Last active December 26, 2015 17:23
Experiments with real-time extraction
(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)
[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 / many-errors.py
Created November 23, 2016 09:01
Large python file full of errors
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
def a(x, y, y):
return t; pass
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>
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
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(-)

Complete log of that session:

$ opam install coq-serapi

The following actions will be performed:
  ⊘ remove    patdiff                    v0.12.1            [uses expect_test_helpers]
  ↗ upgrade   ocaml-migrate-parsetree    1.5.0 to 1.8.0     [required by ppxlib]
  ⊘ remove    core_bench                 v0.12.0            [conflicts with ppx_jane]
  ↗ upgrade   sexplib0                   v0.12.0 to v0.14.0 [required by ppx_sexp_conv]
/// # Getting Started with Dafny: A Guide
///
/// Be sure to follow along with the code examples by clicking the "load
/// in editor" link in the
/// corner. See what the tool says, try to fix programs on your own, and
/// experiment!
///
/// ## Introduction
///
/// Dafny is a language that is designed to make it easy to