[racket] problem with pict->bitmap and mrlib/write-animated-gif

Can't figure it out, but something in the interaction between pict->bitmap and write-animated-gif is causing the frames to display one on top of the other when viewing the gif. #lang racket (require pict mrlib/gif) (define (draw-frame i) (pict->bitmap (circle (* 50 i (write-anima

[racket] proof assistants, DrRacket and Bootstrap

I have a few questions that might be off-topic. Are you interested in formal proofs? Have you considered adapting DrRacket to give an integrated editor for a proof assistant? The proof assistants Coq and Isabelle use jedit and ProofGeneral, which I think aren't nearly as nice as DrRacket. I

[racket] Fwd: JFP CFP

If you're working on parallel or concurrent programming, consider submitting! Robby -- CALL FOR PAPERS JFP Special Issue on

Re: [racket] typed racket and generic interfaces, is there a workaround using properties?

Like this, I think: (but for some reason it seems to print it 3 times?) #lang typed/racket (struct foo () #:transparent #:property prop:custom-write (lambda (this out mode) (displayln "whatever"))) (print (foo)) On Sep 26, 2014, at 11:07 PM, Anthony Carrico wrote: > Dredging up an ol

[racket] proof assistants, DrRacket and Bootstrap

I have a few questions that might be off-topic. Are you interested in formal proofs? Have you considered adapting DrRacket to give an integrated editor for a proof assistant? The proof assistants Coq and Isabelle use jedit and ProofGeneral, which I think aren't nearly as nice as DrRacket. I ac

Re: [racket] typed racket and generic interfaces, is there a workaround using properties?

Actually using prop:dict works (I hadn’t found prop:dict yet when I first asked this) #lang typed/racket (define-type Dict-Ref ([Dict Any] [Any] . ->* . Any)) (define-type Dict-Set! (Dict Any Any . -> . Void)) (define-type Dict-Set (Dict Any Any . -> . Dict)) (define-type Dict-Remove! (Dict Any .

Re: [racket] proof assistants, DrRacket and Bootstrap

To answer the first part of your email, yes. Carl Eastlund developed Dracula for Rackety use of the ACL2 theorem prover. -Ian - Original Message - From: Bill Richter To: users@racket-lang.org Sent: Sat, 27 Sep 2014 03:38:48 -0400 (EDT) Subject: [racket] proof assistants, DrRacket and Boot

[racket] aws/glacier: credential scope

Greetings. I'm trying to use the aws/glacier package, and running into a problem where I'm being told: Credential should be scoped to a valid region, not 'eu-west-1' I'm following the instructions at My test code is:

Re: [racket] proof assistants, DrRacket and Bootstrap

Carl Eastlund developed Dracula for Rackety use of the ACL2 theorem prover. Thanks, Ian! May I suggest that you try to handle Coq, Isabelle or HOL Light? I believe these are the foremost proof assistants. The fields medalist Vladimir Voevodsky uses Coq, in which the 4-color theorem and the

Re: [racket] proof assistants, DrRacket and Bootstrap

Thanks, Prabhakar, this is exactly what I wanted, and you know something about it (I was barely able to install Coq): I am teaching a grad course using Coq right now, and using Proof General within Emacs for it. That is not bad, but I would love to have a DrRacket interface. > OCaml

Re: [racket] proof assistants, DrRacket and Bootstrap

Bill Richter wrote: >Carl Eastlund developed Dracula for Rackety use of the ACL2 theorem >prover. Thanks, Ian! May I suggest that you try to handle Coq, Isabelle or HOL Light? I believe these are the foremost proof assistants. The fields medalist Vladimir Voevodsky uses Coq, in which the 4-c

Re: [racket] proof assistants, DrRacket and Bootstrap

ACL2 [is] probably far and away the theorem prover that has had the most industrial impact Interesting, Prabhakar! I had not heard that before. A DrRacket interface to Coq or Isabelle would, in contrast, be more superficial, in the style of Proof General. I think so, but interface

Re: [racket] problem with pict->bitmap and mrlib/write-animated-gif

Solved, with help from Jens Soegaard; I had to modify mrlib/write-gifs to take a disposal argument, and use it in all calls to gif-add-control. martin On Sat, Sep 27, 2014 at 12:27 AM, Martin DeMello wrote: > Can't figure it out, but something in the interaction between pict->bitmap > and write

Re: [racket] proof assistants, DrRacket and Bootstrap

On 2014-09-27, 5:50 PM, Bill Richter wrote: Thanks, Prabhakar, this is exactly what I wanted, and you know something about it (I was barely able to install Coq): I struggled with installing it also, especially since I'm using a Mac. Racket has spoiled us in that respect. But parsing an

Re: [racket] typed racket and generic interfaces, is there a workaround using properties?

On 09/27/2014 09:49 AM, Alexander D. Knauth wrote: > Like this, I think: (but for some reason it seems to print it 3 times?) > #lang typed/racket > > (struct foo () #:transparent > #:property prop:custom-write > (lambda (this out mode) > (displayln "whatever"))) > > (print (foo)) I didn

Re: [racket] typed racket and generic interfaces, is there a workaround using properties?

On Sat, Sep 27, 2014 at 9:11 PM, Anthony Carrico wrote: > On 09/27/2014 09:49 AM, Alexander D. Knauth wrote: >> Like this, I think: (but for some reason it seems to print it 3 times?) >> #lang typed/racket >> >> (struct foo () #:transparent >> #:property prop:custom-write >> (lambda (this out

Re: [racket] proof assistants, DrRacket and Bootstrap

Translating the gist of suggestions to such posters, I would say: do you really need to execute *any* expression? If not, use OCamllex and/or OCamlyacc (maybe Menhir, or a smaller and cleaner parser combinator library) to write a parser for your language subset, and then write an int

Re: [racket] proof assistants, DrRacket and Bootstrap

On Sep 27, 2014, at 1:38 AM, Bill Richter wrote: > Scheme is well-suited for writing a Scheme interpreter, because of the quote > feature. OCaml doesn't have a quote feature, so the question arises how to > write an OCaml interpreter inside OCaml. That's not quite what I want to do, > but if

Re: [racket] proof assistants, DrRacket and Bootstrap

type ast = VAR of String | LAM of String * ast | APP of ast * ast | CONST of int | ADD of ast * ast type val = BASIC of int | FUNCTION of val -> val | ... Thanks, Matthias! I know this is way off topic, but I think it's the sort of thing only Schemers understand, and I think HOL Ligh