Autoformalize your Math

2. The Linux terminal🔗

Throughout this guide we will mainly work by writting commands in the terminal. In layman terms, the terminal is a way to interact with the computer using only text. You certainly are used to interacting with the computer through graphical applications, clicking with your mouse here and there. In the terminal, there is no need for a mouse: everything is done through text commands. This may seem inconvenient at first, but actually it is a more powerful way to interact with the computer.

I will do everything in the terminal that is characteristic of GNU/Linux distributions. If you use GNU/Linux, great! We are on the same page. If you use MacOS, you are also good to go: the terminal and the operating system are very similar to GNU/Linux. There may be small changes in the commands I use, but Google can easily translate between the commands used here and the ones needed in MacOS. I will try to provide also the MacOS commands when needed, but I cannot guarantee they will work, since I don't have a Mac where I can test them (contributions in this line are welcome!). But what if you have Windows? Then you have to fully uninstall it, and then install a user-friendly GNU/Linux distro like Linux Mint or Ubuntu. Of course, I am (partially) kidding. There is a way to use a terminal like the one in Linux inside Windows. Below I briefly explain how.

2.1. Windows Subsystem for Linux (WSL)🔗

This section is only for the Windows users.

WSL stands for Windows Subsystem for Linux. It is a Microsoft tool that lets you install a Linux distribution inside Windows and run Linux programs, utilities, and Bash commands from there. In practice, it gives you a Linux terminal without asking you to erase Windows, partition your disk, or manually configure a full virtual machine.

If you have Windows 11, or Windows 10 version 2004 or later, the installation is usually very simple. Open PowerShell as administrator, run:

Bashterminal
$
wsl --install

and restart the computer if Windows asks you to do so. By default, this installs Ubuntu. The first time you open it, Windows will finish the installation and ask you to choose a Linux user name and password. If you want another distribution, first run:

Bashterminal
$
wsl --list --online

to see the available options, and then install one of them with, for example:

Bashterminal
$
wsl --install -d Debian

After that, opening a Linux terminal is just opening the Linux distribution you installed. Press the Windows key, type Ubuntu (or Debian, or whatever distribution you chose), and open it like a normal application. You can also open Windows Terminal and choose your Linux distribution from the menu. If you already have PowerShell open, you can type:

Bashterminal
$
wsl

and press enter. When the prompt changes, you are inside the Linux system. To leave it and go back to PowerShell, type:

Bashterminal
$
exit

The official and up-to-date instructions are in the Microsoft WSL installation guide. Use them if any of the commands above fail, because Windows changes faster than this text.

For the purposes of this guide, WSL is more than enough. You can think of it as creating a new Linux system inside your Windows system. When you open WSL, you are not just opening a different-looking window: you are entering that Linux system, with its own files, programs, users, and directories. The safest habit is to do your work inside the home directory of that Linux system, written ~. Put your projects there, install your tools there, and run your commands from there. Windows files are still reachable from WSL, usually under /mnt/c, but we will not use that as our main working place.

2.2. Tasting the terminal🔗

Before we move on to more interesting stuff, let us get a feeling for how the terminal works.

First, open a terminal. In GNU/Linux, look for an application called Terminal, Konsole, GNOME Terminal, or something similar. In MacOS, open the application called Terminal. In Windows, if you followed the previous section, open the Linux distribution that you installed with WSL, for instance Ubuntu.

You should see an almost empty window with one line of text and a cursor waiting for you to type. That line is the prompt. It may look like [user@machine ~]$, or maybe like user@machine:~$.

The exact text does not matter. The prompt is just the shell saying: "I am ready, write a command". The last symbol is often $. You do not have to type it. In this guide, when I write a command, the $ will be shown by the terminal block, but the part you type is only the command itself.

Let us start with the smallest possible test. Type this and press enter:

Bashterminal
$
echo hello
Output
hello

The command is echo hello. The output is hello, the text printed by the command after you press enter. After the output, the prompt appears again. This is the usual rhythm of the terminal: write a command, press enter, read the output, and get a new prompt.

Now ask the terminal who you are:

Bashterminal
$
whoami
Output
username

Of course, your output will not be username, unless your user name happens to be username. It will be the name of your user in that system (inside WSL, your Linux user may have a different name from your Windows user).

Next, ask where you are:

Bashterminal
$
pwd
Output
/home/username

pwd means print working directory. A directory is what graphical interfaces usually call a folder. The working directory is the directory where the terminal is currently standing. Again, your output will probably be different, but it should have the same shape. If you are in a GNU/Linux or WSL system, it will often be something like /home/username.

The directory /home/username is your user's home directory. Since writing that full path all the time would be annoying, the shell uses the symbol ~ as an abbreviation for your home directory. So, when you see ~ in the prompt, it means that you are at home. This is not a metaphor. It means your personal working place in the system.

Let us look around:

Bashterminal
$
ls

ls lists the files and directories in the current directory. If the output is empty, do not worry. It only means that there is nothing visible there yet. If you see names like Desktop, Documents, or Downloads, those are directories.

We can also move to another directory. For instance, if Documents exists, try:

Bashterminal
$
cd Documents

cd means change directory. Notice that this command usually prints nothing. In the terminal, printing nothing often means that the command worked. To check where you are now, run pwd again:

Bashterminal
$
pwd

To go back home, run:

Bashterminal
$
cd ~

(or symply cd) and check again:

Bashterminal
$
pwd

That is enough for now. You have written commands, seen output, moved between directories, and met ~. If the screen starts to feel too full, you can clean it with:

Bashterminal
$
clear

or, in most terminals, pressing at the same time Control and l. This does not delete files or undo anything. It only cleans the terminal window, like erasing a blackboard. The previous commands are still in the shell history, and you can usually bring them back with the up arrow.

I hope you got a feeling for what the terminal is, and what does it look like to work on it. So let's move on to more interesting stuff.