@@ -10,7 +10,7 @@
1010\newcommand{\req}[1][]{\refstepcounter{req}\label{req:#1}\paragraph{\fbox{\textsf{\textsc{REQ}-\thereq}}}}
1111\newcommand{\refreq}[1]{\hyperref[req:#1]{\fbox{\textsf{REQ-\ref*{req:#1}}}}}
1212
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}
1414\author{Kostyuchenko Ilya}
1515\date{}
1616
@@ -26,7 +26,7 @@
2626
2727\section{Purpose}
2828
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.
3030
3131\section{Scope}
3232
@@ -34,8 +34,6 @@ The project consists of developing the following components:
3434
3535\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).
3636
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.
38−
3937\section{Product perspective}
4038
4139\subsection{System interfaces}
@@ -52,11 +50,11 @@ The application does not provide a hardware interface.
5250
5351\subsection{Software interfaces}
5452
55−The application allows interactions through the Language Server Protocol.
53+The application allows interactions through standard UNIX input-output capabilities.
5654
5755\subsection{Communications interfaces}
5856
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.
6058
6159\subsection{Memory}
6260
@@ -64,12 +62,10 @@ The memory required to run the system depends on the size of the project being p
6462
6563\subsection{Operations}
6664
67−The application supports the following operations initiated by the code editor:
65+The application supports the following operations:
6866
6967\begin{enumerate}
7068 \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
7369\end{enumerate}
7470
7571\subsection{Site adaptation requirements}
@@ -85,30 +81,19 @@ No interaction with services in performed.
8581The application provides the following functionality to the user:
8682
8783\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
89− \item While the user is exploring a Nix expression language project the application will provide:
90− \begin{enumerate}
91− \item type information for subexpressions the user is inspecting
92− \item definitions of variables a user is inspecting
93− \end{enumerate}
84+ \item Checks user-supplied programs for type incompatibilities
85+ \item Reports the resulting types of user-supplied expressions
9486\end{enumerate}
9587
9688\section{User characteristics}
9789
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:
99−
100−\begin{enumerate}
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
105−\end{enumerate}
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.
10691
10792\section{Limitations}
10893
10994\subsection{Interface to other applications}
11095
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.
11297
11398\subsection{Criticality of the application}
11499
@@ -125,7 +110,7 @@ The contents of this document assume the following:
125110
126111\section{Apportioning of requirements}
127112
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.
129114
130115\section{Specified requirements}
131116
@@ -137,51 +122,31 @@ The application is a self-contained executable file that, when executed, functio
137122
138123\req[typechecking] The system should perform type checking for expression where under conditions from \refreq{restrictons}.
139124
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.
141−
142125\req The system should analyze the types and presence of attributes in attribute sets under conditions from \refreq{restrictons}.
143126
144−\req The system should report encountered typechecking errors through means defined by the Language Server Protocol.
145−
146−\req The system should provide the location of definitions for all locally used terms under conditions from \refreq{restrictons}.
127+\req The system should report encountered typechecking errors.
147128
148129\req The system should report the use of undefined terms through means defined by the Language Server Protocol under conditions from \refreq{restrictons}.
149130
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}).
151−
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}.
153−
154−\req The system should provide a way for the programmer to explicitly annotate types of expressions which will influence type checking.
155−
156131\section{Usability requirements}
157132
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.
159134
160135\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.
161136
162137\section{Performance requirements}
163138
164−\req The system should process incoming requests within 1 second (the system should formulate a response, not necessarily finish performing the requested action).
165−
166−\req The system should process incoming requests from a single client.
139+\req The system should process incoming requests within 1 minute.
167140
168141\section{External interfaces}
169142
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.
171144
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/}}.
173−
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.
175−
176−\paragraph{The destination of the input} is the code editor the user is using which has requested information about the source code.
177−
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/}}.
145+\paragraph{The purpose} of this interface is to provide easy way to provide programs to typecheck as inputs.
179146
180147\section{Functions}
181148
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.
183−
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.
149+The fundamental functions of the system are queries: get the type of an expression.
185150
186151\subsection{Generating the type of an expression}
187152
@@ -230,7 +195,7 @@ If the context \emph{analysis context} is already generated then the responses a
230195
231196\subsection{Error handling}
232197
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.
234199
235200If the system encounters an internal (as opposed to a user error) the error is written to the standard error output.
236201
@@ -265,7 +230,6 @@ The following approaches and methods are planned to be employed to qualify the s
265230
266231\begin{enumerate}
267232 \item Automated hand-written unit-tests
268− \item Automated randomly generated property tests
269233 \item Manual testing
270234\end{enumerate}
271235