The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
Let's me make a semi-off topic remark because it is an hot topic for me.

When js_of_ocaml made its first buzz, we (especialy Yann Regis Giana)
went throw the code of coq with a chain saw in order to see how hard it
would be to have a purely offline coqtop in a web brower.
It "worked" except that you don't go very far without "Require"!

"Require" is the essential feature that forbids me to make coqtop run in
a sandboxed environment under MacOS. The executable don't run in
sandboxed mode is the reason why Apple rejects my coqIDE.app of the Mac
Store !

Conclusion, an abstraction over Require and an implementation of it that
works when you cannot read where ever you like on the disk would be very
useful but I have no idea.

All the best,
Pierre B.


On 01/09/2014 14:05, Adam Chlipala wrote:
> I think the system we're building could be effective in that context. 
> Our first target audience is beginning computer-science undergraduates,
> to whom we aim to introduce both functional programming and rigorous
> math and proofs.  I wouldn't naturally cover continuous math there, but
> probably the tools would also help with continuous stuff.
> 
> I'll certainly let you know when our public release is ready.
> 
> On 08/31/2014 05:46 PM, Vladimir Voevodsky wrote:
>> I am. In fact we are looking for resources which could be used for a
>> project of the following form:
>>
>>> I have this idea that it would be good to:
>>>
>>> 1. Make a webpage for school kids where they could register, learn
>>> some basic Coq, and solve problems (in Coq).
>>>
>>> 2. To organize a camp where the winners (those who solved most
>>> problems) could go - some with stipends and some paying money.
>>>
>>> 3. Have such camps also organized by other people in other countries.
>>>
>>> 4. Eventually to have a network which will bring talented young
>>> people into math through formal proofs.
>>
>> I had some interesting experience interacting with students at the 8th
>> Asian Science Camp in Singapore last week that resulted, among other
>> things in a poster that can be seen here:
>> https://plus.google.com/+DavidRoberts/posts/SxkdFxR3Uk4?id=6052874823364569762&oid=103404025783539237119
>>
>> Vladimir.
>>
>>
>>
>>
>>
>>
>>
>> On Aug 31, 2014, at 10:15 PM, Adam Chlipala 
>> <adamc AT csail.mit.edu
>> <mailto:adamc AT csail.mit.edu>>
>>  wrote:
>>
>>> We're working on a novice-oriented interface at MIT.  I expect we'll
>>> make a public release in the next month or so.  However, you also
>>> might not be interested in a novice-oriented interface. :)
>>>
>>> On 08/31/2014 05:13 PM, Vladimir Voevodsky wrote:
>>>> Hello,
>>>>
>>>> is there a working web interface for Coq?
>>>>
>>>> When I tried ProofWeb it told me 'Welcome to Coq trunk (Nov. 2006)"
>>>>
>>>> and then it refused to work at all (could not start a new line after
>>>> the first sentence).
>>>>
>>>> Vladimir.
>>>
>>
>