James Wilcox

Feature request: resolve local module aliases in M-.

1

Consider the following file: ``` Module N := Nat. Check N.add. ``` (This code is idiomatic for long module names that have been `Require`d but not `Import`ed.) Placing the cursor...

Folding eats comments before next definition

1

Consider the following code ``` (* a foo is a nat *) Definition foo := nat. (* bar increments a foo *) Definition bar (x : foo) : foo :=...

Fields of Inductive/Record/Class not available in completion

2

Consider the following code ``` Record foofoofoo : Type := { barbarbar : nat }. ``` The type `foofoofoo` is available in completions later in the file, but the field...

What is the best way to avoid stack overflows with recursive generators?

7

I'm new to the library, and I tried reading through the source code and all existing open and closed issues and PRs, but I couldn't find any guidance to this....

The elimination rule for pairs is currently ``` H >> C H(i) = Sig x : A. B H, x : A, y : B >> C ``` Since it...

It would be nice to introduce students to proper logging infrastructure using `@Log`. I think the best place for this would be a short writeup as part of Lab 0,...

I'd like to have a more systematic approach to discovering bugs such as #25. Here's a prototype ``` class Nothing: pass def unreachable(x: Nothing) -> None: pass ``` and then...

This is a trick I stole from a Coq-club post. ``` Ltac break_exists := repeat match goal with | [ H: exists (varname: _), _ |- _ ] => let...

Nondeterministic wrong answers, segfaults, and apparent memory corruptions when passing multiple empty column names to read_csv

2

### What happens? Consider the following call to `read_csv`: ```sql from read_csv('bug.csv', header=false, names=['','']); ``` When run with any table in `bug.csv` with at least two rows and at least...