cpitclaudel

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

cpitclaudel

/// # 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

cpitclaudel

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]

cpitclaudel

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(-)

cpitclaudel

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

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

def a(x, y, y):
    return t; pass

cpitclaudel

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

cpitclaudel

[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

(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)