[racket] users Digest, Vol 109, Issue 65

Please take me off the list

Thanks

On Sat, Sep 27, 2014 at 9:11 PM,  <users-request at racket-lang.org> wrote:
> Send users mailing list submissions to
>         users at racket-lang.org
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         http://lists.racket-lang.org/users/listinfo
> or, via email, send a message with subject or body 'help' to
>         users-request at racket-lang.org
>
> You can reach the person managing the list at
>         users-owner at racket-lang.org
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of users digest..."
>
>
> [Racket Users list:
>  http://lists.racket-lang.org/users ]
>
>
> Today's Topics:
>
>    1. Re: proof assistants, DrRacket and Bootstrap (Bill Richter)
>    2. Re: proof assistants, DrRacket and Bootstrap (Prabhakar Ragde)
>    3. Re: proof assistants, DrRacket and Bootstrap (Bill Richter)
>    4. Re: problem with pict->bitmap and mrlib/write-animated-gif
>       (Martin DeMello)
>    5. Re: proof assistants, DrRacket and Bootstrap (Prabhakar Ragde)
>    6. Re: typed racket and generic interfaces, is there a
>       workaround using properties? (Anthony Carrico)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Sat, 27 Sep 2014 16:50:11 -0500
> From: Bill Richter <richter at math.northwestern.edu>
> To: Prabhakar Ragde <plragde at uwaterloo.ca>
> Cc: users at racket-lang.org
> Subject: Re: [racket] proof assistants, DrRacket and Bootstrap
> Message-ID:
>         <201409272150.s8RLoBQW030663 at poisson.math.northwestern.edu>
>
> 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 doesn't have a quote feature, so the question arises how to
>    > write an OCaml interpreter inside OCaml.
>
>    In my senior undergraduate programming language course, I have them
>    write various interpreters and typecheckers in various languages,
>    including Racket, OCaml, and Haskell.
>    [...]
>
> I know this is way off-topic, but it seems to me that Schemers are the only people who want an elegant solution here:
>
>    But parsing an expression written in faux OCaml/Haskell is quite
>    complicated. [...] Parsing is much easier in Racket/Scheme because
>    of the similarity of code/data and the presence of 'read'.
>
> I think it's a parsing question I'm stuck on.  I think I need to use camlp to avoid the following hack/kludge which I learned from the HOL Light experts, found in my file
> hol_light/RichterHilbertAxiomGeometry/readable.ml
> which is part of the HOL Light distribution:
>
> (* From update_database.ml: Execute any OCaml expression given as a string.  *)
>
> let exec = ignore o Toploop.execute_phrase false Format.std_formatter
>   o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
>
> (* Following miz3.ml, exec_thm returns the theorem representing a string, so *)
> (* exec_thm "FORALL_PAIR_THM";; returns                                      *)
> (* val it : thm = |- !P. (!p. P p) <=> (!p1 p2. P (p1,p2))                   *)
>
> let thm_ref = ref TRUTH;;
>
> let exec_thm s =
>   if Str.string_match (Str.regexp "[^;]*;") s 0 then raise Noparse
>   else
>     try exec ("thm_ref := (("^ s ^"): thm);;");
>       !thm_ref
>     with _ -> raise Noparse;;
>
> When I posted my question on the OCaml list, the experts said don't ever use Obj.magic, but I think they didn't think much of me using Toploop either.
>
> --
> Best,
> Bill
>
>
> ------------------------------
>
> Message: 2
> Date: Sat, 27 Sep 2014 18:00:24 -0400
> From: Prabhakar Ragde <plragde at uwaterloo.ca>
> To: users at racket-lang.org
> Subject: Re: [racket] proof assistants, DrRacket and Bootstrap
> Message-ID: <54273378.1070605 at uwaterloo.ca>
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
>
> 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-color
>> theorem and the Feit-Thompson theorem was formalized by Georges
>> Gonthier.  Tom Hales just finished formalizing his proof of Kepler
>> conjecture in HOL Light and Isabelle (which is HOL as well).  I'm no
>> expert, but I think that ACL2 (also Prover9) is an FOL prover, and
>> the bulk of activity in formal proofs uses type theories.  HOL is
>> simple, it's Church's simple types (a version of the Lambda
>> Calculus), and Coq uses a much more complicated type theory.
>
> I'm sorry, I forgot about Carl's Dracula work when composing my earlier
> reply. ACL2 is more limited, but its advantage (besides being probably
> far and away the theorem prover that has had the most industrial impact)
> is that its language (Applicative Common Lisp, hence the acronym) is
> much closer to Racket, allowing for stronger integration both with
> DrRacket and into a Racket-based curriculum. A DrRacket interface to Coq
> or Isabelle would, in contrast, be more superficial, in the style of
> Proof General. --PR
>
>
> ------------------------------
>
> Message: 3
> Date: Sat, 27 Sep 2014 17:26:44 -0500
> From: Bill Richter <richter at math.northwestern.edu>
> To: Prabhakar Ragde <plragde at uwaterloo.ca>
> Cc: users at racket-lang.org
> Subject: Re: [racket] proof assistants, DrRacket and Bootstrap
> Message-ID:
>         <201409272226.s8RMQiEM030897 at poisson.math.northwestern.edu>
>
>    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 interfaces are really important, and DrRacket has a beautiful interface.
>
> --
> Best,
> Bill
>
>
> ------------------------------
>
> Message: 4
> Date: Sat, 27 Sep 2014 15:46:25 -0700
> From: Martin DeMello <martindemello at gmail.com>
> To: Racket Users List <users at racket-lang.org>
> Subject: Re: [racket] problem with pict->bitmap and
>         mrlib/write-animated-gif
> Message-ID:
>         <CAFrFfuG9GXu+N6Tp6Ccg1-n1QX6KFybMRpyj9p_Drk2+SRcrKw at mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> 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 <martindemello at gmail.com>
> wrote:
>
>> 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-animated-gif
>>  (map draw-frame (sequence->list (in-range 1 10)))
>>  10
>>  "test1.gif"
>>  #:loop? true
>>  #:one-at-a-time? true)
>>
>> martin
>>
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://lists.racket-lang.org/users/archive/attachments/20140927/a42ef6eb/attachment-0001.html>
>
> ------------------------------
>
> Message: 5
> Date: Sat, 27 Sep 2014 18:54:56 -0400
> From: Prabhakar Ragde <plragde at uwaterloo.ca>
> To: Bill Richter <richter at math.northwestern.edu>
> Cc: users at racket-lang.org
> Subject: Re: [racket] proof assistants, DrRacket and Bootstrap
> Message-ID: <54274040.5070902 at uwaterloo.ca>
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
>
> 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 expression written in faux OCaml/Haskell is quite
>>     complicated. [...] Parsing is much easier in Racket/Scheme because
>>     of the similarity of code/data and the presence of 'read'.
>>
>> I think it's a parsing question I'm stuck on.  I think I need to use camlp to avoid the following hack/kludge which I learned from the HOL Light experts, found in my file
>> hol_light/RichterHilbertAxiomGeometry/readable.ml
>> which is part of the HOL Light distribution:
>>
>> (* From update_database.ml: Execute any OCaml expression given as a string.  *)
>
> I don't have enough practice in OCaml to grasp what your code does (and,
> yes, it is way off-topic), but I do know that about once every month or
> two, someone posts to this list about using 'eval' in Racket, and they
> are warned not to use it unless they really know what they are doing and
> have a suitable application (which is rare). That warning probably is
> doubled in a statically-typed language, in which 'eval' should not even
> be possible without subverting the type system (I gather this is what
> you are doing). 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 interpreter for the resulting ASTs. --PR
>
>
> ------------------------------
>
> Message: 6
> Date: Sat, 27 Sep 2014 21:11:08 -0400
> From: Anthony Carrico <acarrico at memebeam.org>
> To: "Alexander D. Knauth" <alexander at knauth.org>
> Cc: racket users list <users at racket-lang.org>
> Subject: Re: [racket] typed racket and generic interfaces, is there a
>         workaround using properties?
> Message-ID: <5427602C.5010101 at memebeam.org>
> Content-Type: text/plain; charset="windows-1252"
>
> 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't realize #:property was legal in typed struct. I guess there
> should be a documentation update here:
>   http://docs.racket-lang.org/ts-reference/special-forms.html
>
> BTW change your program to use the given port: (displayln "whatever"
> out) to avoid the double printing problem, although I'm not exactly sure
> why it would have that effect.
>
> Thanks!
>
> --
> Anthony Carrico
>
>
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: signature.asc
> Type: application/pgp-signature
> Size: 181 bytes
> Desc: OpenPGP digital signature
> URL: <http://lists.racket-lang.org/users/archive/attachments/20140927/63d8e553/attachment.sig>
>
> End of users Digest, Vol 109, Issue 65
> **************************************