Merge branch 'master' of github:/tiyn/wiki

wiki/linux/package_manager/pacman_and_aur.md

@@ -314,8 +314,8 @@ This section is based on a
 
 In this case the error stems from a missing package.
 Normally it can easily be fixed by installing that corresponding package.
-But please note that [pyenv](/wiki/programming_language/golang.md#setup) can hide packages if the
+But please note that [pyenv](/wiki/programming_language/python.md#pyenv-installation) can hide
-global Python version is set to something other than `system`.
+packages if the global Python version is set to something other than `system`.
 This is especially the case on [Arch Linux-systems](/wiki/linux/arch-linux.md) because Python
 packages are also installed via [Pacman or Yay](#arch-linux-pacman-and-yay).
 In this case the global Version has to be changed to `system` or the package installed to the

wiki/programming_language.md

@@ -0,0 +1,16 @@
+# Programming Language
+
+A programming language is a language for expressing computer programs.
+
+## List of Programming Languages
+
+The following is a list of programming languages that are featured in this wiki.
+
+- [C](/wiki/programming_language/c.md)
+- [Go](/wiki/programming_language/go.md)
+- [Nim](/wiki/programming_language/nim.md)
+- [Python](/wiki/programming_language/python.md)
+- [Rocq](/wiki/programming_language/rocq.md)
+- [Rust](/wiki/programming_language/rust.md)
+- [VHDL](/wiki/programming_language/vhdl.md)
+- [Viper](/wiki/programming_language/viper.md)

wiki/programming_language/python.md

@@ -174,21 +174,20 @@ This section addresses the [PyTorch module](https://pytorch.org/).
 Pytorch is a machine learning resource which is often used for
 [neural networks](/wiki/neural_network.md).
 
-#### Setup Pytorch with Cuda for GPU usage
+#### Setup Pytorch with CUDA for GPU usage
 
-Please note that according to
+CUDA is also only available for Nvidia GPUs.
-[various sources](https://www.reddit.com/r/archlinux/comments/1nxipcu/nvidia_pascal/gpu_not_supporting_cuda_13_can_i)
+For AMD GPUs refer to [the ROCm section](#setup-pytorch-with-rocm-for-gpu-usage).
-Cuda 13 does not support nVidia Pascal GPUs.
-In this case an earlier version of Cuda has to be used.
 
 If you are on Arch Linux or a distribution based on it install
 `python-pytorch-cuda` via `pacman -S python-pytorch-cuda`.
 
 After that visit
-[the official pytorch website](https://pytorch.org/get-started/locally/) and
+[the official PyTorch website](https://pytorch.org/get-started/locally) and
-install pytorch for your custom configuration.
+install PyTorch for your custom configuration.
 
-After that try to run the following python script:
+After that try to run the following python script.
+This should give back `True` if the setup was successful and the GPU is available.
 
 ```python
 import torch
@@ -196,7 +195,66 @@ import torch
 torch.cuda.is_available()
 ```
 
-This should give back `True`.
+Please note that according to
+[various sources](https://www.reddit.com/r/archlinux/comments/1nxipcu/nvidia_pascal/gpu_not_supporting_cuda_13_can_i)
+CUDA 13 does not support nVidia Pascal GPUs.
+In this case an earlier version of CUDA has to be used.
+
+#### Setup PyTorch with ROCm for GPU usage
+
+ROCm is also only available for AMD GPUs.
+For Nvidia GPUs refer to [the CUDA section](#setup-pytorch-with-cuda-for-gpu-usage).
+
+For ROCm to work some system packages have to be installed.
+For Linux refer to the
+[official Linux guide](https://rocm.docs.amd.com/projects/radeon-ryzen/en/latest/docs/install/installrad/native_linux/install-radeon.html).
+For [Arch Linux](/wiki/linux/arch-linux.md) although it is not listed the required
+[AUR packages](/wiki/linux/package_manager.md) include `rocm-core`, `rocminfo`, `roctracer` and
+`rccl`.
+For Windows refer to the
+[official Windows guide](https://rocm.docs.amd.com/projects/radeon-ryzen/en/latest/docs/install/installrad/windows/howto_windows.html).
+
+After the systemwide setup the project environment can be setup.
+It is recommended to use [virtual environments](#using-virtual-environments).
+The easiest way to achieve ROCm support is by using [pip](#modules).
+As explained in the 
+[official PyTorch guide](https://rocm.docs.amd.com/projects/radeon-ryzen/en/latest/docs/install/installrad/native_linux/install-pytorch.html)
+the following example can be used inside the environment to install all needed ROCm packages.
+In this example the version `7.2` is installed.
+Adjustments to the command may have to be done in case another version should be installed.
+
+```sh 
+wget https://repo.radeon.com/rocm/manylinux/rocm-rel-7.2/torch-2.9.1%2Brocm7.2.0.lw.git7e1940d4-cp312-cp312-linux_x86_64.whl
+wget https://repo.radeon.com/rocm/manylinux/rocm-rel-7.2/torchvision-0.24.0%2Brocm7.2.0.gitb919bd0c-cp312-cp312-linux_x86_64.whl
+wget https://repo.radeon.com/rocm/manylinux/rocm-rel-7.2/triton-3.5.1%2Brocm7.2.0.gita272dfa8-cp312-cp312-linux_x86_64.whl
+wget https://repo.radeon.com/rocm/manylinux/rocm-rel-7.2/torchaudio-2.9.0%2Brocm7.2.0.gite3c6ee2b-cp312-cp312-linux_x86_64.whl
+pip install \
+torch-2.9.1+rocm7.2.0.lw.git7e1940d4-cp312-cp312-linux_x86_64.whl \
+torchvision-0.24.0+rocm7.2.0.gitb919bd0c-cp312-cp312-linux_x86_64.whl \
+torchaudio-2.9.0+rocm7.2.0.gite3c6ee2b-cp312-cp312-linux_x86_64.whl \
+triton-3.5.1+rocm7.2.0.gita272dfa8-cp312-cp312-linux_x86_64.whl
+```
+
+If old versions of `torch`, `torchvision`, `torchaudio` or `triton` are installed inside the
+environment they may need to be removed.
+
+After this installation for some GPUs - especially integrated GPUs like the Radeon 660M - an
+additional step has to be taken.
+In this case the following global shell variable has to be set.
+
+```sh 
+export HSA_OVERRIDE_GFX_VERSION=10.3.0
+```
+
+After that try to run the following python script.
+Since ROCm uses a bridge to access CUDA it should give back `True` if the setup was successful and
+the GPU is available.
+
+```python
+import torch
+
+torch.cuda.is_available()
+```
 
 ### Hailo
 

wiki/programming_language/rocq.md

@@ -0,0 +1,75 @@
+# Rocq
+
+[Rocq](https://rocq-prover.org/) is an interactive theorem prover.
+It was formerly known as Coq.
+
+## Setup
+
+Rocq can be installed as explained on [the official website](https://rocq-prover.org/install).
+
+The easiest way to install Rocq is by using Opam due to it also being able to manage packages for
+Rocq.
+Opam needs to be installed for this.
+On most [Linux-based Systems](/wiki/linux.md) the [package manager](/wiki/linux/package_manager.md)
+contains a package called `opam`.
+If Opam was not initialized before, do it using the following commands.
+The command may ask to edit the config file for the shell.
+This is needed to function correctly.
+
+```sh
+opam init
+eval $(opam env)
+```
+
+Then Rocq can be installed using the following command.
+`<version>` has to be set to the desired version to install (for example `9.0.0`).
+
+```sh
+opam pin add rocq-prover <version>
+```
+
+## Usage
+
+This section addresses the usage of Rocq.
+
+### Basic Usage
+
+Rocq proves are saved in `.v` files.
+These can be compiled using the following command where `<file>` is a Rocq proof file.
+
+```sh 
+rocq c <file>
+```
+
+If nothing is shown as output and files like a `.vo` file are generated the proof was successful.
+Otherwise it was not successful.
+
+### Examples
+
+The following example proofs can be used to confirm the [Rocq setup](#setup) to work correctly.
+
+The following is a simple proof for commutativity of addition.
+This proof is correct.
+
+```v 
+Theorem plus_comm : forall n m : nat, n + m = m + n.
+Proof.
+  intros n m.
+  induction n as [| n' IH].
+  - simpl. rewrite <- plus_n_O. reflexivity.
+  - simpl. rewrite IH. rewrite <- plus_n_Sm. reflexivity.
+Qed.
+```
+
+The following proof attempts to proof that all natural numbers are equal to zero which is obviously
+false.
+
+```v 
+Theorem all_zero : forall n : nat, n = 0.
+Proof.
+  intros n.
+  destruct n.
+  - reflexivity.
+  - reflexivity.
+Qed.
+```