• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
        • Vl-model
        • Vl-json
        • Vl-gather
        • Vl-server
          • Vl-server-opts-p
            • Parse-vl-server-opts
            • Vl-server-opts
            • Make-vl-server-opts
            • Change-vl-server-opts
            • Honsed-vl-server-opts
            • Make-honsed-vl-server-opts
            • *vl-server-opts-usage*
            • Vl-server-opts->root
            • Vl-server-opts->readme
            • Vl-server-opts->public
            • Vl-server-opts->port
            • Vl-server-opts->mem
            • Vl-server-opts->help
        • Vl-pp
        • Vl-lint
        • Vl-main
        • Vl-toolkit-other-command
        • Vl-help
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-server

Vl-server-opts-p

Options for running vl server.

(vl-server-opts-p x) is a defaggregate of the following fields.

• help — Show a brief usage message and exit.
      Invariant (booleanp help).
• readme — Show a more elaborate README and exit.
      Invariant (booleanp readme).
• mem — Default: 6 GB. How much memory to try to use. Raising this may improve performance by avoiding garbage collection. To avoid swapping, keep this below (physical_memory - 2 GB).
      Invariant (posp mem).
• port — Default: 9999. What port to run on.
      Invariant (posp port).
• root — Default: "./translations". Where to find translations. See the --readme to understand this.
      Invariant (stringp root).
• public — Default: "/v/filer5b/v11q001/acl2/acl2-git-scratch/books/centaur/vl2014/server/public". Where to find the supporting 'public' directory from the module browser's code. You should be able to ignore this unless you're deploying the module browser to a different directory.
      Invariant (stringp public).

Source link: vl-server-opts-p

Subtopics

Parse-vl-server-opts

Parse arguments from the command line into a vl-server-opts-p aggregate.

Vl-server-opts

Raw constructor for vl-server-opts-p structures.

Make-vl-server-opts

Constructor macro for vl-server-opts-p structures.

Change-vl-server-opts

A copying macro that lets you create new vl-server-opts-p structures, based on existing structures.

Honsed-vl-server-opts

Raw constructor for honsed vl-server-opts-p structures.

Make-honsed-vl-server-opts

Constructor macro for honsed vl-server-opts-p structures.

*vl-server-opts-usage*

Automatically generated usage message.

Vl-server-opts->root

Access the root field of a vl-server-opts-p structure.

Vl-server-opts->readme

Access the readme field of a vl-server-opts-p structure.

Vl-server-opts->public

Access the public field of a vl-server-opts-p structure.

Vl-server-opts->port

Access the port field of a vl-server-opts-p structure.

Vl-server-opts->mem

Access the mem field of a vl-server-opts-p structure.

Vl-server-opts->help

Access the help field of a vl-server-opts-p structure.