• 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
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
      • Io
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
        • Osicat
      • Std/io
      • Oslib
      • Bridge
      • Clex
      • Tshell
      • Unsound-eval
      • Hacker
      • ACL2s-interface
      • Startup-banner
      • Command-line
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
      • Osicat
    • Std/io
    • Oslib
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Quicklisp

Osicat

OSICAT is a Quicklisp library providing an OS interface for Unix platforms.

Build Issues

osicat occassionally causes a build to fail with a message like the following:

| HARD ACL2 ERROR in INCLUDE-RAW:  Load of "osicat-raw.lsp" failed with
| the following message:
| File #P"/var/lib/jenkins/workspace/acl2-testing/books/quicklisp/asdf-
| home/cache/common-lisp/ccl-1.12-f98-linux-x64/var/lib/jenkins/workspace/acl2-
| testing/books/quicklisp/bundle/software/osicat-20220220-git/src/osicat.lx64fsl
| " does not exist.

Fix Instructions

Check the timestamps of the files libosicat.so and wrappers__wrapper.o in the directory:

<path-to-acl2>/books/quicklisp/asdf-home/cache/common-lisp/*/<path-to-acl2>/books/quicklisp/bundle/software/osicat-20220220-git/posix/

On Linux, you can use ls -la --time-style=full-iso <file> to see the full timestamp. On macOS, you can use ls -lT <file>.

If the timestamp seconds are different between the two files, this is the issue. The fix is to update the timestamp of wrappers__wrapper.o to fall within the same second as libosicat.so.

On Linux, you can update the timestamp with sudo touch -t <new-time> <file>. See man touch for the formatting of <new-time>. As an example, to set the time to 2023-05-16 23:01:17, <new-time> would be 202305162301.17.

On macOS, you can perform a relative update of the timestamp, adding one second with the command: sudo touch -A 01 <file>.

Explanation

This build issue may occur when two or more books which depend on osicat are being certified simultaneously. A race condition allows one certification to attempt to read the compiled binary while the other is deleting it to rebuild.

The timestamps are compared to check whether some part of osicat needs to be rebuilt. Timestamps are truncated internally to the nearest second and the wrappers__wrapper.o file is considered out of date if its truncated timestamp is earlier than libosicat.so.

Thank you to Eric McCarthy for investigating and debugging this issue.