reloading source code in source code conflicts with the instructions in README

[xieyuheng]

---

hi Carl

it is about the scheme version of j-bob

in j-bob.scm
I see you are using (load "j-bob-lang.scm")

and
in little-prover.scm
you are using (load "j-bob.scm")

and in README.md
you said

;; Load the J-Bob language:
(load "j-bob-lang.scm")
;; Load J-Bob, our little proof assistant:
(load "j-bob.scm")
;; Load the transcript of all proofs in the book:
(load "little-prover.scm")
;; Run every proof in the book, up to and including the proof of align/align:
(dethm.align/align)

---

note that
function redefinition is side effect

thus
this will redefine a lots of primitive functions multiple times
and use these multiple redefined functions to redefine other functions

this hurts performance

as a result
when I follow the instructions in README.md
my scheme interpreter will eat up all the memory of my machine [about 2G of memory]

---

you can fix this in many ways
my advice is to keep the README.md as it is
and do not use (load) in source code

---

[carl-eastlund]

Thanks for the report. I'm aware that loading multiple of these files will redefine a lot of functions. Our intention was that users only need to load one of these files, depending on what set of definitions they need, and each file pulls in whatever dependencies it needs. Perhaps we should clarify that in the README.

I would not have expected you to get to 2G of memory, however. I'd like to figure out how that is happening. I would expect reloading one of these files to redefine the functions in the file, and then the old ones would be garbage collected, so there wouldn't be cumulative memory wasted over time, just a little time wasted once. I would also expect the memory footprint of each file to be relatively small, so that it would take many, many copies of the whole thing to add up to 2G. Somehow, my expectations do not correspond to reality. Do you know what might cause the redefinitions to add up to so much memory usage?

[xieyuheng]

---

what cause the redefinitions to add up to so much memory usage?

---

  ;; as instructed by README.md
  ;; (load "j-bob-lang.scm")

  (define s.car car)

  (define (car x) (if (pair? x) (s.car x) '()))

---

  ;; as instructed by README.md
  ;; (load "j-bob.scm")
  ;; in j-bob.scm
  ;; (load "j-bob-lang.scm") [again]

  (define s.car car)
  ;; "s.car" should denotes "the primitive car of scheme"
  ;;   [forgive me to abuse double quote here]
  ;; but at this point
  ;; it is already not "the primitive car of scheme"
  ;; but is "the car of j-bob-lang"
  ;; note that
  ;;   "the car of j-bob-lang"
  ;;   runs slower then
  ;;   "the primitive car of scheme"

  ;; thus the following is "the car of j-bob-lang"
  ;; but runs slower then "the previous car of j-bob-lang"
  (define (car x) (if (pair? x) (s.car x) '()))

  ;; and all the functions in j-bob.scm
  ;; are composed by the slower version of functions

---

  ;; as instructed by README.md
  ;; (load "little-prover.scm")
  ;; in little-prover.scm
  ;; (load "j-bob.scm") [again]

  ;; you see how things get even worse here

---

[xieyuheng]

---

Our intention was that
users only need to load one of these files,
depending on what set of definitions they need,
and each file pulls in whatever dependencies it needs.

---

IMO
the feature you need here is the module system of a programming language

for example
a simple idea is

when

  (need "cicada.scm")

record the file "cicada.scm" as been loaded

and
when

  (need "cicada.scm") ;; again

just ignore it

note that
the calling to the function "need" can be nested
so recursive function should be used to implement it

---

[carl-eastlund]

Yep, I'm aware that R5RS Scheme lacks a module system. It's unfortunate. We used R5RS because the previous books in the series are compatible with it, and we didn't have to bring in details of a module system like Racket's or R6RS's or so on and so forth. Module systems are fantastic, but beyond the scope of a little book like this one. So we're making do with the semantics of load in Scheme.

You're right that I picked the wrong default. I've switched the files to not load each other, so you can load them yourself in sequence and they won't interfere with each other. Thanks again for bringing this to my attention, and sorry for the difficulties.

[xieyuheng]

glad that I can help ^-^
I am a fans of the little books