Please take me off the list Thanks
On Sat, Sep 27, 2014 at 9:11 PM, <users-requ...@racket-lang.org> wrote: > Send users mailing list submissions to > users@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-requ...@racket-lang.org > > You can reach the person managing the list at > users-ow...@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 <rich...@math.northwestern.edu> > To: Prabhakar Ragde <plra...@uwaterloo.ca> > Cc: users@racket-lang.org > Subject: Re: [racket] proof assistants, DrRacket and Bootstrap > Message-ID: > <201409272150.s8rlobqw030...@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 <plra...@uwaterloo.ca> > To: users@racket-lang.org > Subject: Re: [racket] proof assistants, DrRacket and Bootstrap > Message-ID: <54273378.1070...@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 <rich...@math.northwestern.edu> > To: Prabhakar Ragde <plra...@uwaterloo.ca> > Cc: users@racket-lang.org > Subject: Re: [racket] proof assistants, DrRacket and Bootstrap > Message-ID: > <201409272226.s8rmqiem030...@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 <martindeme...@gmail.com> > To: Racket Users List <users@racket-lang.org> > Subject: Re: [racket] problem with pict->bitmap and > mrlib/write-animated-gif > Message-ID: > <cafrffug9gxu+n6tp6ccg1-n1qx6kfybmrpyj9p_drk2+src...@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 <martindeme...@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 <plra...@uwaterloo.ca> > To: Bill Richter <rich...@math.northwestern.edu> > Cc: users@racket-lang.org > Subject: Re: [racket] proof assistants, DrRacket and Bootstrap > Message-ID: <54274040.5070...@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 <acarr...@memebeam.org> > To: "Alexander D. Knauth" <alexan...@knauth.org> > Cc: racket users list <users@racket-lang.org> > Subject: Re: [racket] typed racket and generic interfaces, is there a > workaround using properties? > Message-ID: <5427602c.5010...@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 > ************************************** ____________________ Racket Users list: http://lists.racket-lang.org/users
