diff --git a/wiki/linux/package_manager/pacman_and_aur.md b/wiki/linux/package_manager/pacman_and_aur.md index de3c225..c172395 100644 --- a/wiki/linux/package_manager/pacman_and_aur.md +++ b/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 -global Python version is set to something other than `system`. +But please note that [pyenv](/wiki/programming_language/python.md#pyenv-installation) can hide +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 diff --git a/wiki/programming_language.md b/wiki/programming_language.md new file mode 100644 index 0000000..8587807 --- /dev/null +++ b/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) diff --git a/wiki/programming_language/c-language.md b/wiki/programming_language/c.md similarity index 100% rename from wiki/programming_language/c-language.md rename to wiki/programming_language/c.md diff --git a/wiki/programming_language/golang.md b/wiki/programming_language/go.md similarity index 100% rename from wiki/programming_language/golang.md rename to wiki/programming_language/go.md diff --git a/wiki/programming_language/python.md b/wiki/programming_language/python.md index ba0f01c..e1a1ba4 100644 --- a/wiki/programming_language/python.md +++ b/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 -[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. +CUDA is also only available for Nvidia GPUs. +For AMD GPUs refer to [the ROCm section](#setup-pytorch-with-rocm-for-gpu-usage). 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 -install pytorch for your custom configuration. +[the official PyTorch website](https://pytorch.org/get-started/locally) and +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 diff --git a/wiki/programming_language/rocq.md b/wiki/programming_language/rocq.md new file mode 100644 index 0000000..21724fb --- /dev/null +++ b/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. +`` has to be set to the desired version to install (for example `9.0.0`). + +```sh +opam pin add rocq-prover +``` + +## 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 `` is a Rocq proof file. + +```sh +rocq c +``` + +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. +```