• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
      • Osicat
    • Oslib
    • Std/io
    • 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. This can be done with the command touch -r wrappers__wrapper.o libosicat.so (the -r flag stands for ``reference''; the command changes the timestamp of wrappers_wrapper.o to match that of libosicat.so).

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.