gilbo

I've just been using whatever emacs (spacemacs really) and proof general feed by default to coqtop. I will try some of those out and let you know if I'm still...

We're just using this very bare-bones repository I threw together: https://github.com/gilbo/hott_reading_group I added a `_CoqProject` file with most of the options you mentioned (I left various warnings on in case...

Thanks for the test case. Unfortunately, I'm too busy right now to fix Cork up properly. I have some printouts of geometric rounding papers on my desk but it'll take...

That's very strange. Can you tell me what order the coordinates your model uses are? Is it very far from the origin? There is a slight quantization for the purposes...

Ahh, I just noticed you're on Windows. In all likelihood there's something weird about how MPIR is being used that's breaking the code. This is very likely to be an...

Did you verify that MPIR is working? I don't have a test binary ready. I can try to poke around my windows box later. > On Jul 27, 2014, at...

You need to provide some member functions in the vert and tri data structs, but I don't remember which off the top of my head. The compiler will yell at...

Since a lot of the code is template code, that’s unsurprising that adding the structs could cause an error. I’m not sure what’s going wrong from the errors you posted....

Look at this part of the error: "already defined in cork.obj" The problem is that you're trying to link files with redundant (possibly conflicting!) definitions of the mesh. > On...

Ok, here’s the quick simple answer from scanning the library (haven’t looked at the code in a while) Notice the following include structure: cork.cpp includes mesh.h includes cork.h main.cpp includes...