write-acl2-code-size

(defun write-acl2-code-size-fn
  (infile outfile ctx state)
  (mv-let (channel state)
    (open-input-channel infile :object state)
    (cond ((null channel) (pprogn (warning$ ctx
            nil
            "Unable to open file ~x0 for input.  Skipping ~
                        computation of code size."
            infile)
          (value nil)))
      (t (er-let* ((lines-code (read-object channel state)) (chars-code (read-object channel state))
            (lines-comm (read-object channel state))
            (chars-comm (read-object channel state))
            (lines-blank (read-object channel state))
            (chars-blank (read-object channel state))
            (lines-total (read-object channel state))
            (chars-total (read-object channel state))
            (lines-doc (read-object channel state))
            (chars-doc (read-object channel state)))
          (let ((state (close-input-channel channel state)))
            (mv-let (ch state)
              (open-output-channel outfile :character state)
              (cond ((null ch) (er soft ctx "Unable to open file ~x0 for output." outfile))
                (t (pprogn (princ$ "Source files (not including doc.lisp):" ch state)
                    (newline ch state)
                    (princ$ "------------------------------------" ch state)
                    (fms "  CODE LINES:~| ~c0 lines, ~c1 characters"
                      (list (cons #\0 (cons lines-code 7))
                        (cons #\1 (cons chars-code 9)))
                      ch
                      state
                      nil)
                    (fms "  COMMENT LINES:~| ~c0 lines, ~c1 characters"
                      (list (cons #\0 (cons lines-comm 7))
                        (cons #\1 (cons chars-comm 9)))
                      ch
                      state
                      nil)
                    (fms "  BLANK LINES:~| ~c0 lines, ~c1 characters"
                      (list (cons #\0 (cons lines-blank 7))
                        (cons #\1 (cons chars-blank 9)))
                      ch
                      state
                      nil)
                    (fms "  TOTAL:~| ~c0 lines, ~c1 characters"
                      (list (cons #\0 (cons lines-total 7))
                        (cons #\1 (cons chars-total 9)))
                      ch
                      state
                      nil)
                    (newline ch state)
                    (princ$ "------------------------------------" ch state)
                    (fms "Documentation (file books/system/doc/acl2-doc.lisp):~| ~
                     ~c0 lines, ~c1 characters~|"
                      (list (cons #\0 (cons lines-doc 7))
                        (cons #\1 (cons chars-doc 9)))
                      ch
                      state
                      nil)
                    (princ$ "------------------------------------" ch state)
                    (newline ch state)
                    (close-output-channel ch state)
                    (value t)))))))))))