@@ -10,7 +10,7 @@
10\newcommand{\req}[1][]{\refstepcounter{req}\label{req:#1}\paragraph{\fbox{\textsf{\textsc{REQ}-\thereq}}}}
10\newcommand{\req}[1][]{\refstepcounter{req}\label{req:#1}\paragraph{\fbox{\textsf{\textsc{REQ}-\thereq}}}}
11\newcommand{\refreq}[1]{\hyperref[req:#1]{\fbox{\textsf{REQ-\ref*{req:#1}}}}}
11\newcommand{\refreq}[1]{\hyperref[req:#1]{\fbox{\textsf{REQ-\ref*{req:#1}}}}}
13−\title{Technical Specification for the Language Server for the Nix Expression Language}
13+\title{Technical Specification for the Static Analyzer for the Nix Expression Language}
14\author{Kostyuchenko Ilya}
14\author{Kostyuchenko Ilya}
@@ -26,7 +26,7 @@
27\section{Purpose}
27\section{Purpose}
29−The purpose of Tix is to simplify development in the Nix expression language.
29+The purpose of the \emph{Static analyzer for the Nix Expression Language} (later referred to as \emph{Tix} for brevity) is to simplify development in the Nix expression language.
31\section{Scope}
31\section{Scope}
@@ -34,8 +34,6 @@ The project consists of developing the following components:
35\paragraph{The Tix type checker} is a program which is designed to statically analyze the given Nix expression language source code and deduce the types of subexpressions used within while detecting some errors made by the programmer (type mismatch errors, which usually arise due to programming mistakes).
35\paragraph{The Tix type checker} is a program which is designed to statically analyze the given Nix expression language source code and deduce the types of subexpressions used within while detecting some errors made by the programmer (type mismatch errors, which usually arise due to programming mistakes).
37−\paragraph{The Tix language server} is a program which implements the Language Server Protocol and is used to integrate the Tix type checker with existing code editors to aid with development.
39\section{Product perspective}
37\section{Product perspective}
41\subsection{System interfaces}
39\subsection{System interfaces}
@@ -52,11 +50,11 @@ The application does not provide a hardware interface.
53\subsection{Software interfaces}
51\subsection{Software interfaces}
55−The application allows interactions through the Language Server Protocol.
53+The application allows interactions through standard UNIX input-output capabilities.
57\subsection{Communications interfaces}
55\subsection{Communications interfaces}
59−The application communicates with the code editor process through the Language Server Protocol using JSON-RPC requests. These requests can be over the network or local to the machine – however, the user decides to set it up.
57+The application communicates with the user by reading input from the file system or terminal emulator, and outputting results to the standard UNIX output handle.
61\subsection{Memory}
59\subsection{Memory}
@@ -64,12 +62,10 @@ The memory required to run the system depends on the size of the project being p
65\subsection{Operations}
63\subsection{Operations}
67−The application supports the following operations initiated by the code editor:
65+The application supports the following operations:
69\begin{enumerate}
67\begin{enumerate}
70 \item Typecheck the current file and report errors
68 \item Typecheck the current file and report errors
71− \item Go to the definition of a variable
72− \item Identify the type of a selected expression expression
73\end{enumerate}
69\end{enumerate}
75\subsection{Site adaptation requirements}
71\subsection{Site adaptation requirements}
@@ -85,30 +81,19 @@ No interaction with services in performed.
85The application provides the following functionality to the user:
81The application provides the following functionality to the user:
87\begin{enumerate}
83\begin{enumerate}
88− \item While the user is editing a Nix expression language file the application will indicate potentially incorrect subexpressions based on type mismatches
84+ \item Checks user-supplied programs for type incompatibilities
89− \item While the user is exploring a Nix expression language project the application will provide:
85+ \item Reports the resulting types of user-supplied expressions
91− \item type information for subexpressions the user is inspecting
92− \item definitions of variables a user is inspecting
94\end{enumerate}
86\end{enumerate}
96\section{User characteristics}
88\section{User characteristics}
98−The user of the application will need intermediate technical skills to set up the application to work with their text editor of choice. More precisely, the user will need to have the following (approximate and incomplete) list of skills:
90+The user of the application will need intermediate technical skills to set up the program. More precisely, the user will need to have basic understanding of how to use their operating system and command line.
101− \item Understand on a high level what a language server is and its role in code editing
102− \item Be familiar with the repositories of packages for their text editor of choice
103− \item Be able to perform intermediate configuration of their text editor of choice and installed packages
104− \item Have basic server administration skills if they are planning to run the server remotely
107\section{Limitations}
92\section{Limitations}
109\subsection{Interface to other applications}
94\subsection{Interface to other applications}
111−The integration with the text editor of choice should be compatible with version 3.15 of the Language Server Protocol.
96+Other applications can be interfaced with through standard input-output handles.
113\subsection{Criticality of the application}
98\subsection{Criticality of the application}
@@ -125,7 +110,7 @@ The contents of this document assume the following:
126\section{Apportioning of requirements}
111\section{Apportioning of requirements}
128−The application is a self-contained executable file that, when executed, functions as a standalone language server. The only requirement that the application externally imposes is the requirement to set up the language sever to function with the desired text editor. There already exist numerous implementation for language server support for many text editors.
113+The application is a self-contained executable file that, when executed, functions as a typechecker.
130\section{Specified requirements}
115\section{Specified requirements}
@@ -137,51 +122,31 @@ The application is a self-contained executable file that, when executed, functio
138\req[typechecking] The system should perform type checking for expression where under conditions from \refreq{restrictons}.
123\req[typechecking] The system should perform type checking for expression where under conditions from \refreq{restrictons}.
140−\req The system should analyze conditional statements where the condition consists only of type checks and boolean operators built into the Nix expression language.
142\req The system should analyze the types and presence of attributes in attribute sets under conditions from \refreq{restrictons}.
125\req The system should analyze the types and presence of attributes in attribute sets under conditions from \refreq{restrictons}.
144−\req The system should report encountered typechecking errors through means defined by the Language Server Protocol.
127+\req The system should report encountered typechecking errors.
146−\req The system should provide the location of definitions for all locally used terms under conditions from \refreq{restrictons}.
148\req The system should report the use of undefined terms through means defined by the Language Server Protocol under conditions from \refreq{restrictons}.
129\req The system should report the use of undefined terms through means defined by the Language Server Protocol under conditions from \refreq{restrictons}.
150−\req The system should report the types of requested expressions through means defined by the Language Server Protocol if the type of the requested expression is unambiguously inferable during typechecking (\refreq{typechecking}).
152−\req The system should provide code completions suggestions from the variables currently in scope and expressions built into the language under conditions from \refreq{restrictons}.
154−\req The system should provide a way for the programmer to explicitly annotate types of expressions which will influence type checking.
156\section{Usability requirements}
131\section{Usability requirements}
158−\req The system should be able to process expressions using the nixpkgs repository.
133+\req The system should be able to process expressions from the nixpkgs repository.
160\req The system should never fail in unrecoverable ways in external imported expressions – if there are type errors in external code the system should resolve the errors automatically.
135\req The system should never fail in unrecoverable ways in external imported expressions – if there are type errors in external code the system should resolve the errors automatically.
162\section{Performance requirements}
137\section{Performance requirements}
164−\req The system should process incoming requests within 1 second (the system should formulate a response, not necessarily finish performing the requested action).
139+\req The system should process incoming requests within 1 minute.
166−\req The system should process incoming requests from a single client.
168\section{External interfaces}
141\section{External interfaces}
170−The only external interface of the system is the Language Server Protocol.
143+The only external interfaces of the system are standard input-output handles.
172−\paragraph{The purpose} of this interface is to provide easy interoperability with a wide range of potential code editors a user might want to use\footnote{\url{https://microsoft.github.io/language-server-protocol/implementors/tools/}}.
145+\paragraph{The purpose} of this interface is to provide easy way to provide programs to typecheck as inputs.
174−\paragraph{The source of input} is the code editor the user uses sending requesting information about the semantics of the file currently being edited in response to the actions the user is taking while browsing or editing source code in the Nix expression language.
176−\paragraph{The destination of the input} is the code editor the user is using which has requested information about the source code.
178−\paragraph{Data and command formats} are defined by the Language Server Protocol\footnote{\url{https://microsoft.github.io/language-server-protocol/specifications/specification-current/}}.
180\section{Functions}
147\section{Functions}
182−The fundamental functions of the system are queries: get the type of an expression, get the definition of a variable, get code completion. All of the responses to the queries can be generated from an \emph{analysis context} which is generated from the current file the user is viewing and any other files it imports.
149+The fundamental functions of the system are queries: get the type of an expression.
184−If the context \emph{analysis context} is already generated then the responses are formulated as follows. If the \emph{analysis context} is not present, then it is generated prior to processing the request.
186\subsection{Generating the type of an expression}
151\subsection{Generating the type of an expression}
@@ -230,7 +195,7 @@ If the context \emph{analysis context} is already generated then the responses a
231\subsection{Error handling}
196\subsection{Error handling}
233−If the system encounters a typing error in the user's code, then the error is returned to the user through means defined in the Language Serer Protocol.
198+If the system encounters a typing error in the user's code, then the error is returned to the user.
235If the system encounters an internal (as opposed to a user error) the error is written to the standard error output.
200If the system encounters an internal (as opposed to a user error) the error is written to the standard error output.
@@ -265,7 +230,6 @@ The following approaches and methods are planned to be employed to qualify the s
266\begin{enumerate}
231\begin{enumerate}
267 \item Automated hand-written unit-tests
232 \item Automated hand-written unit-tests
268− \item Automated randomly generated property tests
269 \item Manual testing
233 \item Manual testing
270\end{enumerate}
234\end{enumerate}