• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
          • World
          • Io
          • Wormhole
          • Programming-with-state
            • Error-triple
            • Cbd
            • State-global-let*
            • Last-prover-steps
            • @
            • Assign
            • Read-run-time
              • Get-real-time
              • Get-cpu-time
              • Canonical-pathname
              • F-put-global
              • Unsound-eval
              • Setenv$
              • Er-progn
              • Read-ACL2-oracle
              • With-live-state
              • F-get-global
              • Getenv$
              • Pprogn
              • Get-real-time
              • Makunbound-global
              • Get-cpu-time
                • F-boundp-global
                • Probe-file
              • W
              • Set-state-ok
              • Random$
            • Mutual-recursion
            • Memoize
            • Mbe
            • Io
            • Defpkg
            • Apply$
            • Loop$
            • Programming-with-state
              • Error-triple
              • Cbd
              • State-global-let*
              • Last-prover-steps
              • @
              • Assign
              • Read-run-time
                • Get-real-time
                • Get-cpu-time
                • Canonical-pathname
                • F-put-global
                • Unsound-eval
                • Setenv$
                • Er-progn
                • Read-ACL2-oracle
                • With-live-state
                • F-get-global
                • Getenv$
                • Pprogn
                • Get-real-time
                • Makunbound-global
                • Get-cpu-time
                  • F-boundp-global
                  • Probe-file
                • Arrays
                • Characters
                • Time$
                • Defmacro
                • Loop$-primer
                • Fast-alists
                • Defconst
                • Evaluation
                • Guard
                • Equality-variants
                • Compilation
                • Hons
                • ACL2-built-ins
                • Developers-guide
                • System-attachments
                • Advanced-features
                • Set-check-invariant-risk
                • Numbers
                • Efficiency
                • Irrelevant-formals
                • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
                • Redefining-programs
                • Lists
                • Invariant-risk
                • Errors
                • Defabbrev
                • Conses
                • Alists
                • Set-register-invariant-risk
                • Strings
                • Program-wrapper
                • Get-internal-time
                • Basics
                • Packages
                • Oracle-eval
                • Defmacro-untouchable
                • <<
                • Primitive
                • Revert-world
                • Unmemoize
                • Set-duplicate-keys-action
                • Symbols
                • Def-list-constructor
                • Easy-simplify-term
                • Defiteration
                • Fake-oracle-eval
                • Defopen
                • Sleep
              • Operational-semantics
              • Real
              • Start-here
              • Debugging
              • Miscellaneous
              • Output-controls
              • Macros
              • Interfacing-tools
            • Interfacing-tools
            • Hardware-verification
            • Software-verification
            • Math
            • Testing-utilities
          • Programming-with-state
          • ACL2-built-ins
          • Read-run-time

          Get-cpu-time

          Read elapsed cpu time

          (Get-cpu-time state) returns the elapsed cpu time in seconds since the start of the current ACL2 session. See read-run-time for further documentation.

          Function: get-cpu-time

          (defun get-cpu-time (state)
            (declare (xargs :stobjs state))
            (read-run-time state))