Author Archives: admin

Capturing Firefox Memory Dumps Using Task Manager

Posted on by
Reply

I am running Windows 7 x64 and used the task manager to capture a dump by using the “Create Dump File” context menu command on my Firefox 11 beta process that had frozen when I exited (window disappeared, but process remained – with 75% CPU usage). Visual C++ Express 2010 complained that “You cannot debug a 64-bit dump of a 32-bit process, you must collect a 32-bit dump of a 32-bit process.” That’s when I found this post  which mentioned that the 32-bit task manager is actually available at C:\Windows\SysWOW64\taskmgr.exe and should be used instead.

Coq Cannot Match Over Arbitrary Propositions

Posted on by
Reply

While working on the Lists section of Software Foundations, I tried to define member as follows:

Definition member (v:nat) (s:bag) : bool :=
match gt (count v s) 0 with
| False => false
| True => true
end.

I kept getting “Error: This clause is redundant.” After some digging around, I found Adam’s explanation that logical propositions (Prop) such as gt (count v s) 0 are not usable for pattern matching in Gallina (without solving “the halting problem and more”). The easier solution then hit me (duh):

Definition member (v:nat) (s:bag) : bool :=
match count v s with
| O => false
| _ => true
end.

Thankfully, I learned something new about Prop though :).

Coq’s Require Import vs Require Export

Posted on by
Reply

The difference between Require Import MyModule and Require Export MyModule is well explained in the modules tutorial:

If a required module depends on other modules then the latter’s are automatically required beforehand. However their contents are not automatically visible. If you want a module M required in a module N to be automatically visible when N is required, you should use Require Export M in your module N.