From c8f79542b1ec72d5985d8d8b72ff79e7ca13cf93 Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 4 Jan 2024 02:19:52 -0500 Subject: [PATCH] feat: include path extension helper & test --- Alloy/C/Server/Worker.lean | 128 +++++++++++++++++++++++++++++++------ test.sh | 2 +- tests/run/includePath.h | 1 + tests/run/includePath.lean | 12 ++++ 4 files changed, 122 insertions(+), 21 deletions(-) create mode 100644 tests/run/includePath.h create mode 100644 tests/run/includePath.lean diff --git a/Alloy/C/Server/Worker.lean b/Alloy/C/Server/Worker.lean index 76da5f4..fd02506 100644 --- a/Alloy/C/Server/Worker.lean +++ b/Alloy/C/Server/Worker.lean @@ -9,22 +9,24 @@ import Alloy.C.Server.Clangd import Alloy.Util.Server /-! -# C Language Server Worker +# Alloy's C Language Server Worker -The language server can be in one of three states: -* `none`: Failed to start and is therefore unsupported -* `some`: Initialized and is running -* `undef`: Not yet started, waiting for the first `getLs?` to attempt start +Alloy uses `clangd` to provide interactive support for C shims. +This file contains the `ClangdWorker` specialization of Alloy's general +`LsWorker` type with additional configuration and helpers for managing +precisely an Alloy-style `clangd` language server. -We use the limbo state of `undef` to ensure we do not try to start the -language server when unnecessary (e.g., during compilation, where elaboration -is non-interactive). +It also contains the definitions for the the `ClangdWorker` instance +used by Alloy in the Lean language server. The instance is also reused during +command elaboration to provide diagnostics for C shim code. -/ -open Lean Lsp +open System Lean Lsp namespace Alloy.C +/-! ## Clangd-specific Worker Configuration & Helpers -/ + /-- Verbosity of the log messages `clangd` writes. -/ inductive ClangdLogging | /-- Error messages only -/ error @@ -40,17 +42,28 @@ def ClangdLogging.toString : ClangdLogging → String instance : ToString ClangdLogging := ⟨ClangdLogging.toString⟩ -/-- Alloy `clangd` language server configuration. -/ +/-- `clangd` language server configuration. -/ structure ServerConfig where /-- - Flags to configure the `clangd` server with. - Alloy adds Lean's include directory to the include path by default. + Array of directories to add to `clangd`'s include path + (e.g., directories to search within for `#include`'d files). + + Alloy initializes this with Lean's include directory by default. + Additional include paths can be added via the `addServerIncludePath` helper. + -/ + includePaths : Array FilePath + /-- + Additional Flags to configure the `clangd` server with + (on top of those implied by `includePaths`). -/ - flags : Array String + moreFlags : Array String /--Log message verbosity of the `clangd` language server. -/ logging : ClangdLogging deriving Inhabited +@[inline] def ServerConfig.flags (cfg : ServerConfig) : Array String := + cfg.includePaths.map (s!"-I{·}") ++ cfg.moreFlags + structure ClangdDocState where leanVer : Nat := 0 shimEndPos : String.Pos := 0 @@ -61,7 +74,7 @@ structure ClangdDocState where abbrev ClangdWorker := LsWorker ClangdDocState -/-- Attempt to initialize the Alloy `clangd` server. -/ +/-- Attempt to initialize an Alloy `clangd` server. -/ def initLs? (cfg : ServerConfig) : BaseIO (Option ClangdWorker) := let act : IO ClangdWorker := do let args := #[s!"--log={cfg.logging}", @@ -179,15 +192,37 @@ def ClangdWorker.collectShimDiagnostics else IO.wait p.result -/-- Configuration with which to start Alloy's C language server. -/ +/-! ## Language Server Instance + +The language server used by Alloy can be in one of three states: +* `none`: Failed to start and is therefore unsupported +* `some`: Initialized and is running +* `undef`: Not yet started, waiting for the first `getLs?` to attempt start + +We use the limbo state of `undef` to ensure we do not try to start the +language server when unnecessary (e.g., during compilation, where elaboration +is non-interactive). +-/ + +/-- +The reference to Alloy's C language sever instance. + +It is wrapped in a mutex because it is has complex volatile state, +but accessed concurrently by the Lean language server. +-/ +initialize serverMux : IO.Mutex (LOption ClangdWorker) ← IO.Mutex.new .undef + +/-- Configuration with which to start Alloy's C language server instance. -/ initialize serverConfig : IO.Ref ServerConfig ← do IO.mkRef { - flags := #["-I", (← Lean.getBuildDir) / "include" |>.toString] + includePaths := #[(← Lean.getBuildDir) / "include"] + moreFlags := #[] logging := .error } -initialize serverMux : IO.Mutex (LOption ClangdWorker) ← IO.Mutex.new .undef - -/-- Return the C language server. Tries to start it exactly once. -/ +/-- +Return Alloy's C language server. +Tries to start it exactly once across all calls to this function. +-/ def getLs? : BaseIO (Option ClangdWorker) := serverMux.atomically fun ref => ref.get >>= fun | .none => return none @@ -197,8 +232,61 @@ def getLs? : BaseIO (Option ClangdWorker) := ref.set ls?.toLOption return ls? -/-- Return the C language server if it has already started. -/ +/-- Return Alloy's C language server if it has already started. -/ def getStartedLs? : BaseIO (Option ClangdWorker) := serverMux.atomically fun ref => ref.get >>= fun | .some ls => return some ls | _ => return none + +/-- +Add an include path to Alloy's C language server configuration. + +### Example + +Consider a library with its header files located at `/lib/include` +where one such header file is `foo.h`. +There are two ways to use this function to add `/lib/include` to the `clangd` +include path for Alloy's C language server so that `foo.h` can be included +via `alloy c include "foo.h"`. + +The most robust approach is to use an `initialize` command to add the +include path to the configuration during module initialization. This will make +the path available whenever a another module imports the module with the +`initialize`. + +**V1/A.lean** +``` +import Alloy.C +initialize Alloy.C.addServerIncludePath "/lib/include" +``` + +**V1/B.lean** +``` +import V1.A +alloy c include "foo.h" +``` + +However, this approach requires two modules. To add to the include path +and make use of it in the same module, one can used an `#eval` command, +but this has some limitations. + +**V2.lean** +``` +import Alloy.C +#eval Alloy.C.addServerIncludePath "/lib/include" +alloy c include "foo.h" +``` + +This will only work if the `#eval` is executed before Alloy +starts the language server. If the `#eval` is executed afterwards, it will +have no effect as Alloy never restarts the language server. + +Alloy starts the language server for C commands where +`Alloy.C.shimDiagnostics.serverOnly` has been set to `false` and in an +interactive context after the file is elaborated once. +Thus, the safest way to make use of such an `#eval` is to put it at the start +of a file before any shim code and to restart the language sever (e.g., via the +`Restart File` command in VSCode) anytime the command is edited. +-/ +@[inline] def addServerIncludePath (path : FilePath) : IO PUnit := do + serverConfig.modify fun cfg => {cfg with includePaths := cfg.includePaths.push path} diff --git a/test.sh b/test.sh index ef8bfc7..4751d2f 100755 --- a/test.sh +++ b/test.sh @@ -15,6 +15,6 @@ pushd tests/compile ./test.sh popd -find tests/run -type f | xargs -n1 ${LAKE:-lake} env lean +find tests/run -type f -name "*.lean" | xargs -n1 ${LAKE:-lake} env lean echo "all done" diff --git a/tests/run/includePath.h b/tests/run/includePath.h new file mode 100644 index 0000000..19627e4 --- /dev/null +++ b/tests/run/includePath.h @@ -0,0 +1 @@ +#define FOOBAR 1 diff --git a/tests/run/includePath.lean b/tests/run/includePath.lean new file mode 100644 index 0000000..e717716 --- /dev/null +++ b/tests/run/includePath.lean @@ -0,0 +1,12 @@ +import Alloy.C +open Alloy.C + +open Lean Elab Command in +#eval show CommandElabM _ from do + let leanFile ← IO.FS.realPath <| System.FilePath.mk (← getFileName) + let includeDir := leanFile.parent.get! + logInfo includeDir.toString + addServerIncludePath includeDir + +set_option Alloy.shimDiagnostics.serverOnly false in +alloy c include "includePath.h"